Clean up some import lists

coq-community · Nov 13, 2024 · 5e1d123 · 5e1d123
1 parent 1fc1c88
commit 5e1d123
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/theories/heaps.v b/theories/heaps.v
@@ -15,11 +15,11 @@
     along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
 
+From Coq Require Import Eqdep.
 From HB Require Import structures.
-From mathcomp Require Import ssreflect ssrfun ssrnat div ssrbool seq.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
 From LemmaOverloading Require Import prelude finmap ordtype.
-From mathcomp Require Import path eqtype.
-Require Import Eqdep.
+From mathcomp Require Import path.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.

diff --git a/theories/prelude.v b/theories/prelude.v
@@ -15,8 +15,8 @@
     along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
 
-Require Import Eqdep ClassicalFacts.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrfun seq.
+From Coq Require Import Eqdep ClassicalFacts.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype seq.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.

diff --git a/theories/rels.v b/theories/rels.v
@@ -15,8 +15,8 @@
     along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
 
+From Coq Require Import Setoid.
 From mathcomp Require Import ssreflect ssrfun ssrbool seq.
-Require Import Setoid.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.