FSets/Msets: some renaming of module params to simplify the task of the extraction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13239 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 8 insertions, 7 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.