1 files changed, 4 insertions, 4 deletions
diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v
index 439f0e5289..c3d614eebc 100644
--- a/theories/FSets/FSetCompat.v
+++ b/theories/FSets/FSetCompat.v
@@ -173,8 +173,6 @@ Module Backport_Sets
 
   Include Backport_WSets E M.
 
-  Module E := E.
-
   Implicit Type s : t.
   Implicit Type x y : elt.
 
@@ -213,6 +211,8 @@ Module Backport_Sets
     [ apply EQ | apply LT | apply GT ]; auto.
   Defined.
 
+  Module E := E.
+
 End Backport_Sets.
 
 
@@ -346,8 +346,6 @@ Module Update_Sets
                     with Definition E.lt := E.lt)
  <: MSetInterface.Sets with Module E:=E.
 
-  Module E := E.
-
   Include Update_WSets E M.
 
   Implicit Type s : t.
@@ -407,4 +405,6 @@ Module Update_Sets
   Lemma compare_spec : forall s s', CompSpec eq lt s s' (compare s s').
   Proof. intros; unfold compare; destruct M.compare; auto. Qed.
 
+  Module E := E.
+
 End Update_Sets.