Skip to content

Commit

Permalink
Qualify module paths in DirectedSets.v
Browse files Browse the repository at this point in the history
  • Loading branch information
Columbus240 committed Feb 6, 2021
1 parent 8245a52 commit a9ea3a3
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions theories/ZornsLemma/DirectedSets.v
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
Require Export Relation_Definitions.
From Coq Require Export Relation_Definitions.
From ZornsLemma Require Import Relation_Definitions_Implicit.
Require Import Classical.
Require Import Arith.
From Coq Require Import Classical.
From Coq Require Import Arith.

Record DirectedSet := {
DS_set : Type;
Expand Down

0 comments on commit a9ea3a3

Please sign in to comment.