Fix compilation on v8.10

coq-community · Aug 19, 2021 · 30fe1f7 · 30fe1f7
1 parent 2f0a479
commit 30fe1f7
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/theories/ZornsLemma/Families.v b/theories/ZornsLemma/Families.v
@@ -1,10 +1,9 @@
 From Coq Require Import Classical_Prop.
 From Coq Require Import Classical_sets.
-From Coq Require Export Ensembles.
-From ZornsLemma Require Import EnsemblesImplicit.
 From ZornsLemma Require Export EnsemblesSpec EnsemblesTactics.
 From ZornsLemma Require Import Image ImageImplicit.
-
+From ZornsLemma Require Import EnsemblesImplicit.
+From Coq Require Export Ensembles.
 Set Implicit Arguments.
 
 Section Families.