3 files changed, 11 insertions, 10 deletions
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 8d6ca420b..25ce5577e 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -321,8 +321,6 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
     exists e; unfold For_all in |- *; eauto.
   Qed.
 
-  Module E := E.
-
   Definition elt := elt.
   Definition t := t.
 
@@ -346,6 +344,8 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
   Definition lt_not_eq := lt_not_eq.
   Definition compare := compare.
 
+  Module E := E.
+
 End DepOfNodep.
 
 
@@ -783,7 +783,6 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
   Qed.
 
 
-  Module E := E.
   Definition elt := elt.
   Definition t := t.
 
@@ -809,4 +808,6 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
   Definition lt_not_eq := lt_not_eq.
   Definition compare := compare.
 
+  Module E := E.
+
 End NodepOfDep.
diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v
index 439f0e528..c3d614eeb 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.
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index 6de91dacc..851237d8f 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -545,9 +545,9 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.
 
 End WRaw2SetsOn.
 
-Module WRaw2Sets (E:DecidableType)(M:WRawSets E) <: WSets with Module E := E.
-  Module E := E.
-  Include WRaw2SetsOn E M.
+Module WRaw2Sets (D:DecidableType)(M:WRawSets D) <: WSets with Module E := D.
+  Module E := D.
+  Include WRaw2SetsOn D M.
 End WRaw2Sets.
 
 (** Same approach for ordered sets *)