suite tentative pour permettre l'utilisation de modules de FSets

avec <: au lieu de : sans surprise de modules genre Raw partout 
ou autres alias dépliés



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

6 files changed, 225 insertions, 217 deletions

diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index cdc5e8d33..cb2a03cf2 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -1785,19 +1785,19 @@ Qed.
 (** Induction over cardinals *)
 
 Lemma sorted_subset_cardinal : forall l' l : list X.t,
- MX.Sort l -> MX.Sort l' ->
- (forall x : elt, MX.In x l -> MX.In x l') -> (length l <= length l')%nat.
+ sort X.lt l -> sort X.lt l' ->
+ (forall x : elt, InA X.eq x l -> InA X.eq x l') -> (length l <= length l')%nat.
 Proof.
  simple induction l'; simpl in |- *; intuition.
  destruct l; trivial; intros.
- absurd (MX.In t nil); intuition.
+ absurd (InA X.eq t nil); intuition.
  inversion_clear H2.
  inversion_clear H1.
  destruct l0; simpl in |- *; intuition.
  inversion_clear H0.
  apply le_n_S.
  case (X.compare t a); intro.
- absurd (MX.In t (a :: l)).
+ absurd (InA X.eq t (a :: l)).
  intro.
  inversion_clear H0.
  order.
@@ -1807,7 +1807,7 @@ Proof.
  firstorder.
  apply H; auto.
  intros.
- assert (MX.In x (a :: l)).
+ assert (InA X.eq x (a :: l)).
  apply H2; auto.
  inversion_clear H6; auto.
  assert (X.lt t x).
@@ -1817,7 +1817,7 @@ Proof.
  simpl in |- *; omega.
  apply (H (t :: l0)); auto.
  intros.
- assert (MX.In x (a :: l)); firstorder.
+ assert (InA X.eq x (a :: l)); firstorder.
  inversion_clear H6; auto.
  assert (X.lt a x).
  apply MX.Sort_Inf_In with (t :: l0); auto.
@@ -2208,7 +2208,7 @@ Hint Constructors sorted_e.
 
 Lemma in_app :
  forall (x : elt) (l1 l2 : list elt),
- L.MX.In x (l1 ++ l2) -> L.MX.In x l1 \/ L.MX.In x l2.
+ InA X.eq x (l1 ++ l2) -> InA X.eq x l1 \/ InA X.eq x l2.
 Proof.
  simple induction l1; simpl in |- *; intuition.
  inversion_clear H0; auto.
@@ -2216,7 +2216,7 @@ Proof.
 Qed.
 
 Lemma in_flatten_e :
- forall (x : elt) (e : enumeration), L.MX.In x (flatten_e e) -> In_e x e.
+ forall (x : elt) (e : enumeration), InA X.eq x (flatten_e e) -> In_e x e.
 Proof.
  simple induction e; simpl in |- *; intuition.
  inversion_clear H.
@@ -2226,9 +2226,9 @@ Proof.
 Qed.
 
 Lemma sort_app :
- forall l1 l2 : list elt, L.MX.Sort l1 -> L.MX.Sort l2 ->
- (forall x y : elt, L.MX.In x l1 -> L.MX.In y l2 -> X.lt x y) ->
- L.MX.Sort (l1 ++ l2).
+ forall l1 l2 : list elt, sort X.lt l1 -> sort X.lt l2 ->
+ (forall x y : elt, InA X.eq x l1 -> InA X.eq y l2 -> X.lt x y) ->
+ sort X.lt (l1 ++ l2).
 Proof.
  simple induction l1; simpl in |- *; intuition.
  apply cons_sort; auto.
@@ -2240,7 +2240,7 @@ Proof.
 Qed.
 
 Lemma sorted_flatten_e :
- forall e : enumeration, sorted_e e -> L.MX.Sort (flatten_e e).
+ forall e : enumeration, sorted_e e -> sort X.lt (flatten_e e).
 Proof.
  simple induction e; simpl in |- *; intuition.
  apply cons_sort.
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 90539ff05..9ac7b9c7c 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -109,7 +109,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
 
   Definition elements :
     forall s : t,
-    {l : list elt | ME.Sort l /\ (forall x : elt, In x s <-> ME.In x l)}.
+    {l : list elt | sort E.lt l /\ (forall x : elt, In x s <-> InA E.eq x l)}.
    Proof.
      intros; exists (elements s); intuition.   
    Defined. 
@@ -394,17 +394,17 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
 
   Definition elements (s : t) : list elt := let (l, _) := elements s in l. 
  
-  Lemma elements_1 : forall (s : t) (x : elt), In x s -> ME.In x (elements s).
+  Lemma elements_1 : forall (s : t) (x : elt), In x s -> InA E.eq x (elements s).
   Proof. 
     intros; unfold elements in |- *; case (M.elements s); firstorder.
   Qed.
 
-  Lemma elements_2 : forall (s : t) (x : elt), ME.In x (elements s) -> In x s.
+  Lemma elements_2 : forall (s : t) (x : elt), InA E.eq x (elements s) -> In x s.
   Proof. 
     intros s x; unfold elements in |- *; case (M.elements s); firstorder.
   Qed.
 
-  Lemma elements_3 : forall s : t, ME.Sort (elements s).  
+  Lemma elements_3 : forall s : t, sort E.lt (elements s).  
   Proof. 
     intros; unfold elements in |- *; case (M.elements s); firstorder.
   Qed.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 0edb009cf..2b9548fe4 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -131,7 +131,7 @@ Proof.
 split; [apply exists_1 | apply exists_2]; auto.
 Qed.
 
-Lemma elements_iff : In x s <-> ME.In x (elements s).
+Lemma elements_iff : In x s <-> InA E.eq x (elements s).
 Proof. 
 split; [apply elements_1 | apply elements_2].
 Qed.
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index ac26d5786..51771fc41 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -199,6 +199,8 @@ Module Raw (X: OrderedType).
 
   (** ** Proofs of set operation specifications. *)
 
+  Section ForNotations.
+
   Notation Sort := (sort X.lt).
   Notation Inf := (lelistA X.lt).
   Notation In := (InA X.eq).
@@ -1020,6 +1022,9 @@ Module Raw (X: OrderedType).
   destruct (e1 a0); auto.
   Defined.
 
+  End ForNotations. 
+  Hint Constructors lt.
+
 End Raw.
 
 (** * Encapsulation
@@ -1030,209 +1035,208 @@ End Raw.
 Module Make (X: OrderedType) <: S with Module E := X.
 
  Module Raw := Raw X. 
- Import Raw.
  Module E := X.
 
- Record slist : Set :=  {this :> Raw.t; sorted : sort X.lt this}.
+ Record slist : Set :=  {this :> Raw.t; sorted : sort E.lt this}.
  Definition t := slist. 
- Definition elt := X.t.
+ Definition elt := E.t.
  
- Definition In (x : elt) (s : t) : Prop := InA X.eq x s.(this).
+ Definition In (x : elt) (s : t) : Prop := InA E.eq x s.(this).
  Definition Equal (s s':t) : Prop := forall a : elt, In a s <-> In a s'.
  Definition Subset (s s':t) : Prop := forall a : elt, In a s -> In a s'.
  Definition Empty (s:t) : Prop := forall a : elt, ~ In a s.
  Definition For_all (P : elt -> Prop)(s:t) : Prop := forall x, In x s -> P x.
  Definition Exists (P : elt -> Prop)(s:t) : Prop := exists x, In x s /\ P x.
 
- Definition mem (x : elt) (s : t) : bool := mem x s.
- Definition add (x : elt)(s : t) : t := Build_slist (add_sort (sorted s) x).
- Definition remove (x : elt)(s : t) : t := Build_slist (remove_sort (sorted s) x).
- Definition singleton (x : elt) : t  := Build_slist (singleton_sort x).
+ Definition mem (x : elt) (s : t) : bool := Raw.mem x s.
+ Definition add (x : elt)(s : t) : t := Build_slist (Raw.add_sort (sorted s) x).
+ Definition remove (x : elt)(s : t) : t := Build_slist (Raw.remove_sort (sorted s) x).
+ Definition singleton (x : elt) : t  := Build_slist (Raw.singleton_sort x).
  Definition union (s s' : t) : t :=
-   Build_slist (union_sort (sorted s) (sorted s')). 
+   Build_slist (Raw.union_sort (sorted s) (sorted s')). 
  Definition inter (s s' : t) : t :=
-   Build_slist (inter_sort (sorted s) (sorted s')). 
+   Build_slist (Raw.inter_sort (sorted s) (sorted s')). 
  Definition diff (s s' : t) : t :=
-   Build_slist (diff_sort (sorted s) (sorted s')). 
- Definition equal (s s' : t) : bool := equal s s'. 
- Definition subset (s s' : t) : bool := subset s s'.
- Definition empty : t := Build_slist empty_sort.
- Definition is_empty (s : t) : bool := is_empty s.
- Definition elements (s : t) : list elt := elements s.
- Definition min_elt (s : t) : option elt := min_elt s.
- Definition max_elt (s : t) : option elt := max_elt s.
- Definition choose (s : t) : option elt  := choose s.
- Definition fold (B : Set) (f : elt -> B -> B) (s : t) : B -> B := fold (B:=B) f s. 
- Definition cardinal (s : t) : nat := cardinal s.
+   Build_slist (Raw.diff_sort (sorted s) (sorted s')). 
+ Definition equal (s s' : t) : bool := Raw.equal s s'. 
+ Definition subset (s s' : t) : bool := Raw.subset s s'.
+ Definition empty : t := Build_slist Raw.empty_sort.
+ Definition is_empty (s : t) : bool := Raw.is_empty s.
+ Definition elements (s : t) : list elt := Raw.elements s.
+ Definition min_elt (s : t) : option elt := Raw.min_elt s.
+ Definition max_elt (s : t) : option elt := Raw.max_elt s.
+ Definition choose (s : t) : option elt  := Raw.choose s.
+ Definition fold (B : Set) (f : elt -> B -> B) (s : t) : B -> B := Raw.fold (B:=B) f s. 
+ Definition cardinal (s : t) : nat := Raw.cardinal s.
  Definition filter (f : elt -> bool) (s : t) : t :=
-   Build_slist (filter_sort (sorted s) f).
- Definition for_all (f : elt -> bool) (s : t) : bool := for_all f s.
- Definition exists_ (f : elt -> bool) (s : t) : bool := exists_ f s.
+   Build_slist (Raw.filter_sort (sorted s) f).
+ Definition for_all (f : elt -> bool) (s : t) : bool := Raw.for_all f s.
+ Definition exists_ (f : elt -> bool) (s : t) : bool := Raw.exists_ f s.
  Definition partition (f : elt -> bool) (s : t) : t * t :=
-   let p := partition f s in
-   (Build_slist (this:=fst p) (partition_sort_1 (sorted s) f),
-   Build_slist (this:=snd p) (partition_sort_2 (sorted s) f)).
- Definition eq (s s' : t) : Prop := eq s s'.
- Definition lt (s s' : t) : Prop := lt s s'.
+   let p := Raw.partition f s in
+   (Build_slist (this:=fst p) (Raw.partition_sort_1 (sorted s) f),
+   Build_slist (this:=snd p) (Raw.partition_sort_2 (sorted s) f)).
+ Definition eq (s s' : t) : Prop := Raw.eq s s'.
+ Definition lt (s s' : t) : Prop := Raw.lt s s'.
 
  Section Spec. 
   Variable s s' s'': t.
   Variable x y : elt.
 
-  Lemma In_1 : X.eq x y -> In x s -> In y s. 
-  Proof. exact (fun H H' => MX.In_eq H H'). Qed.
+  Lemma In_1 : E.eq x y -> In x s -> In y s. 
+  Proof. exact (fun H H' => Raw.MX.In_eq H H'). Qed.
  
   Lemma mem_1 : In x s -> mem x s = true.
-  Proof. exact (fun H => mem_1 s.(sorted) H). Qed.
+  Proof. exact (fun H => Raw.mem_1 s.(sorted) H). Qed.
   Lemma mem_2 : mem x s = true -> In x s. 
-  Proof. exact (fun H => mem_2 H). Qed.
+  Proof. exact (fun H => Raw.mem_2 H). Qed.
  
   Lemma equal_1 : Equal s s' -> equal s s' = true.
-  Proof. exact (equal_1 s.(sorted) s'.(sorted)). Qed.
+  Proof. exact (Raw.equal_1 s.(sorted) s'.(sorted)). Qed.
   Lemma equal_2 : equal s s' = true -> Equal s s'.
-  Proof. exact (fun H => equal_2 H). Qed.
+  Proof. exact (fun H => Raw.equal_2 H). Qed.
 
   Lemma subset_1 : Subset s s' -> subset s s' = true.
-  Proof. exact (subset_1 s.(sorted) s'.(sorted)). Qed.
+  Proof. exact (Raw.subset_1 s.(sorted) s'.(sorted)). Qed.
   Lemma subset_2 : subset s s' = true -> Subset s s'.
-  Proof. exact (fun H => subset_2 H). Qed.
+  Proof. exact (fun H => Raw.subset_2 H). Qed.
 
   Lemma empty_1 : Empty empty.
-  Proof. exact empty_1. Qed.
+  Proof. exact Raw.empty_1. Qed.
 
   Lemma is_empty_1 : Empty s -> is_empty s = true. 
-  Proof. exact (fun H => is_empty_1 H). Qed.
+  Proof. exact (fun H => Raw.is_empty_1 H). Qed.
   Lemma is_empty_2 : is_empty s = true -> Empty s.
-  Proof. exact (fun H => is_empty_2 H). Qed.
+  Proof. exact (fun H => Raw.is_empty_2 H). Qed.
  
-  Lemma add_1 : X.eq x y -> In y (add x s).
-  Proof. exact (fun H => add_1 s.(sorted) H). Qed.
+  Lemma add_1 : E.eq x y -> In y (add x s).
+  Proof. exact (fun H => Raw.add_1 s.(sorted) H). Qed.
   Lemma add_2 : In y s -> In y (add x s).
-  Proof. exact (fun H => add_2 s.(sorted) x H). Qed.
-  Lemma add_3 : ~ X.eq x y -> In y (add x s) -> In y s. 
-  Proof. exact (fun H => add_3 s.(sorted) H). Qed.
-
-  Lemma remove_1 : X.eq x y -> ~ In y (remove x s).
-  Proof. exact (fun H => remove_1 s.(sorted) H). Qed.
-  Lemma remove_2 : ~ X.eq x y -> In y s -> In y (remove x s).
-  Proof. exact (fun H H' => remove_2 s.(sorted) H H'). Qed.
+  Proof. exact (fun H => Raw.add_2 s.(sorted) x H). Qed.
+  Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s. 
+  Proof. exact (fun H => Raw.add_3 s.(sorted) H). Qed.
+
+  Lemma remove_1 : E.eq x y -> ~ In y (remove x s).
+  Proof. exact (fun H => Raw.remove_1 s.(sorted) H). Qed.
+  Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
+  Proof. exact (fun H H' => Raw.remove_2 s.(sorted) H H'). Qed.
   Lemma remove_3 : In y (remove x s) -> In y s.
-  Proof. exact (fun H => remove_3 s.(sorted) H). Qed.
+  Proof. exact (fun H => Raw.remove_3 s.(sorted) H). Qed.
 
-  Lemma singleton_1 : In y (singleton x) -> X.eq x y. 
-  Proof. exact (fun H => singleton_1 H). Qed.
-  Lemma singleton_2 : X.eq x y -> In y (singleton x). 
-  Proof. exact (fun H => singleton_2 H). Qed.
+  Lemma singleton_1 : In y (singleton x) -> E.eq x y. 
+  Proof. exact (fun H => Raw.singleton_1 H). Qed.
+  Lemma singleton_2 : E.eq x y -> In y (singleton x). 
+  Proof. exact (fun H => Raw.singleton_2 H). Qed.
 
   Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
-  Proof. exact (fun H => union_1 s.(sorted) s'.(sorted) H). Qed.
+  Proof. exact (fun H => Raw.union_1 s.(sorted) s'.(sorted) H). Qed.
   Lemma union_2 : In x s -> In x (union s s'). 
-  Proof. exact (fun H => union_2 s.(sorted) s'.(sorted) H). Qed.
+  Proof. exact (fun H => Raw.union_2 s.(sorted) s'.(sorted) H). Qed.
   Lemma union_3 : In x s' -> In x (union s s').
-  Proof. exact (fun H => union_3 s.(sorted) s'.(sorted) H). Qed.
+  Proof. exact (fun H => Raw.union_3 s.(sorted) s'.(sorted) H). Qed.
 
   Lemma inter_1 : In x (inter s s') -> In x s.
-  Proof. exact (fun H => inter_1 s.(sorted) s'.(sorted) H). Qed.
+  Proof. exact (fun H => Raw.inter_1 s.(sorted) s'.(sorted) H). Qed.
   Lemma inter_2 : In x (inter s s') -> In x s'.
-  Proof. exact (fun H => inter_2 s.(sorted) s'.(sorted) H). Qed.
+  Proof. exact (fun H => Raw.inter_2 s.(sorted) s'.(sorted) H). Qed.
   Lemma inter_3 : In x s -> In x s' -> In x (inter s s').
-  Proof. exact (fun H => inter_3 s.(sorted) s'.(sorted) H). Qed.
+  Proof. exact (fun H => Raw.inter_3 s.(sorted) s'.(sorted) H). Qed.
 
   Lemma diff_1 : In x (diff s s') -> In x s. 
-  Proof. exact (fun H => diff_1 s.(sorted) s'.(sorted) H). Qed.
+  Proof. exact (fun H => Raw.diff_1 s.(sorted) s'.(sorted) H). Qed.
   Lemma diff_2 : In x (diff s s') -> ~ In x s'.
-  Proof. exact (fun H => diff_2 s.(sorted) s'.(sorted) H). Qed.
+  Proof. exact (fun H => Raw.diff_2 s.(sorted) s'.(sorted) H). Qed.
   Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').
-  Proof. exact (fun H => diff_3 s.(sorted) s'.(sorted) H). Qed.
+  Proof. exact (fun H => Raw.diff_3 s.(sorted) s'.(sorted) H). Qed.
  
   Lemma fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A),
       fold f s i = fold_left (fun a e => f e a) (elements s) i.
-  Proof. exact (fold_1 s.(sorted)). Qed.
+  Proof. exact (Raw.fold_1 s.(sorted)). Qed.
 
   Lemma cardinal_1 : cardinal s = length (elements s).
-  Proof. exact (cardinal_1 s.(sorted)). Qed.
+  Proof. exact (Raw.cardinal_1 s.(sorted)). Qed.
 
   Section Filter.
   
   Variable f : elt -> bool.
 
-  Lemma filter_1 : compat_bool X.eq f -> In x (filter f s) -> In x s. 
-  Proof. exact (@filter_1 s x f). Qed.
-  Lemma filter_2 : compat_bool X.eq f -> In x (filter f s) -> f x = true. 
-  Proof. exact (@filter_2 s x f). Qed.
+  Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s. 
+  Proof. exact (@Raw.filter_1 s x f). Qed.
+  Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true. 
+  Proof. exact (@Raw.filter_2 s x f). Qed.
   Lemma filter_3 :
-      compat_bool X.eq f -> In x s -> f x = true -> In x (filter f s).
-  Proof. exact (@filter_3 s x f). Qed.
+      compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
+  Proof. exact (@Raw.filter_3 s x f). Qed.
 
   Lemma for_all_1 :
-      compat_bool X.eq f ->
+      compat_bool E.eq f ->
       For_all (fun x => f x = true) s -> for_all f s = true.
-  Proof. exact (@for_all_1 s f). Qed.
+  Proof. exact (@Raw.for_all_1 s f). Qed.
   Lemma for_all_2 :
-      compat_bool X.eq f ->
+      compat_bool E.eq f ->
       for_all f s = true -> For_all (fun x => f x = true) s.
-  Proof. exact (@for_all_2 s f). Qed.
+  Proof. exact (@Raw.for_all_2 s f). Qed.
 
   Lemma exists_1 :
-      compat_bool X.eq f ->
+      compat_bool E.eq f ->
       Exists (fun x => f x = true) s -> exists_ f s = true.
-  Proof. exact (@exists_1 s f). Qed.
+  Proof. exact (@Raw.exists_1 s f). Qed.
   Lemma exists_2 :
-      compat_bool X.eq f ->
+      compat_bool E.eq f ->
       exists_ f s = true -> Exists (fun x => f x = true) s.
-  Proof. exact (@exists_2 s f). Qed.
+  Proof. exact (@Raw.exists_2 s f). Qed.
 
   Lemma partition_1 :
-      compat_bool X.eq f -> Equal (fst (partition f s)) (filter f s).
-  Proof. exact (@partition_1 s f). Qed.
+      compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s).
+  Proof. exact (@Raw.partition_1 s f). Qed.
   Lemma partition_2 :
-      compat_bool X.eq f ->
+      compat_bool E.eq f ->
       Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
-  Proof. exact (@partition_2 s f). Qed.
+  Proof. exact (@Raw.partition_2 s f). Qed.
 
   End Filter.
 
-  Lemma elements_1 : In x s -> InA X.eq x (elements s).
-  Proof. exact (fun H => elements_1 H). Qed.
-  Lemma elements_2 : InA X.eq x (elements s) -> In x s.
-  Proof. exact (fun H => elements_2 H). Qed.
-  Lemma elements_3 : sort X.lt (elements s).
-  Proof. exact (elements_3 s.(sorted)). Qed.
+  Lemma elements_1 : In x s -> InA E.eq x (elements s).
+  Proof. exact (fun H => Raw.elements_1 H). Qed.
+  Lemma elements_2 : InA E.eq x (elements s) -> In x s.
+  Proof. exact (fun H => Raw.elements_2 H). Qed.
+  Lemma elements_3 : sort E.lt (elements s).
+  Proof. exact (Raw.elements_3 s.(sorted)). Qed.
 
   Lemma min_elt_1 : min_elt s = Some x -> In x s. 
-  Proof. exact (fun H => min_elt_1 H). Qed.
-  Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ X.lt y x. 
-  Proof. exact (fun H => min_elt_2 s.(sorted) H). Qed.
+  Proof. exact (fun H => Raw.min_elt_1 H). Qed.
+  Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x. 
+  Proof. exact (fun H => Raw.min_elt_2 s.(sorted) H). Qed.
   Lemma min_elt_3 : min_elt s = None -> Empty s.
-  Proof. exact (fun H => min_elt_3 H). Qed.
+  Proof. exact (fun H => Raw.min_elt_3 H). Qed.
 
   Lemma max_elt_1 : max_elt s = Some x -> In x s. 
-  Proof. exact (fun H => max_elt_1 H). Qed.
-  Lemma max_elt_2 : max_elt s = Some x -> In y s -> ~ X.lt x y. 
-  Proof. exact (fun H => max_elt_2 s.(sorted) H). Qed.
+  Proof. exact (fun H => Raw.max_elt_1 H). Qed.
+  Lemma max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y. 
+  Proof. exact (fun H => Raw.max_elt_2 s.(sorted) H). Qed.
   Lemma max_elt_3 : max_elt s = None -> Empty s.
-  Proof. exact (fun H => max_elt_3 H). Qed.
+  Proof. exact (fun H => Raw.max_elt_3 H). Qed.
 
   Lemma choose_1 : choose s = Some x -> In x s.
-  Proof. exact (fun H => choose_1 H). Qed.
+  Proof. exact (fun H => Raw.choose_1 H). Qed.
   Lemma choose_2 : choose s = None -> Empty s.
-  Proof. exact (fun H => choose_2 H). Qed.
+  Proof. exact (fun H => Raw.choose_2 H). Qed.
 
   Lemma eq_refl : eq s s.
-  Proof. exact (eq_refl s). Qed.
+  Proof. exact (Raw.eq_refl s). Qed.
   Lemma eq_sym : eq s s' -> eq s' s.
-  Proof. exact (@eq_sym s s'). Qed.
+  Proof. exact (@Raw.eq_sym s s'). Qed.
   Lemma eq_trans : eq s s' -> eq s' s'' -> eq s s''.
-  Proof. exact (@eq_trans s s' s''). Qed.
+  Proof. exact (@Raw.eq_trans s s' s''). Qed.
 
   Lemma lt_trans : lt s s' -> lt s' s'' -> lt s s''.
-  Proof. exact (@lt_trans s s' s''). Qed.
+  Proof. exact (@Raw.lt_trans s s' s''). Qed.
   Lemma lt_not_eq : lt s s' -> ~ eq s s'.
-  Proof. exact (lt_not_eq s.(sorted) s'.(sorted)). Qed.
+  Proof. exact (Raw.lt_not_eq s.(sorted) s'.(sorted)). Qed.
 
   Definition compare : Compare lt eq s s'.
   Proof.
-  elim (compare s.(sorted) s'.(sorted));
+  elim (Raw.compare s.(sorted) s'.(sorted));
    [ constructor 1 | constructor 2 | constructor 3 ]; 
    auto. 
   Defined.
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 130d31d1d..2b6017c5e 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -114,7 +114,7 @@ Module Raw (X: DecidableType).
      end.
 
   (** ** Proofs of set operation specifications. *)
-
+  Section ForNotations. 
   Notation NoDup := (NoDupA X.eq).
   Notation In := (InA X.eq).
 
@@ -750,6 +750,7 @@ Module Raw (X: DecidableType).
   unfold eq, Equal; firstorder.
   Qed.
 
+  End ForNotations.
 End Raw.
 
 (** * Encapsulation
@@ -760,176 +761,175 @@ End Raw.
 Module Make (X: DecidableType) <: S with Module E := X.
 
  Module Raw := Raw X. 
- Import Raw.
  Module E := X.
 
- Record slist : Set :=  {this :> Raw.t; unique : NoDupA X.eq this}.
+ Record slist : Set :=  {this :> Raw.t; unique : NoDupA E.eq this}.
  Definition t := slist. 
- Definition elt := X.t.
+ Definition elt := E.t.
  
- Definition In (x : elt) (s : t) := InA X.eq x s.(this).
- Definition Equal (s s':t) := forall a : elt, In a s <-> In a s'.
- Definition Subset (s s':t) := forall a : elt, In a s -> In a s'.
- Definition Empty (s:t) := forall a : elt, ~ In a s.
- Definition For_all (P : elt -> Prop) (s : t) :=
+ Definition In (x : elt) (s : t) : Prop := InA E.eq x s.(this).
+ Definition Equal (s s':t) : Prop := forall a : elt, In a s <-> In a s'.
+ Definition Subset (s s':t) : Prop := forall a : elt, In a s -> In a s'.
+ Definition Empty (s:t) : Prop := forall a : elt, ~ In a s.
+ Definition For_all (P : elt -> Prop) (s : t) : Prop :=
    forall x : elt, In x s -> P x.
- Definition Exists (P : elt -> Prop) (s : t) := exists x : elt, In x s /\ P x.
+ Definition Exists (P : elt -> Prop) (s : t) : Prop := exists x : elt, In x s /\ P x.
 
- Definition mem (x : elt) (s : t) : bool := mem x s.
- Definition add (x : elt)(s : t) : t  := Build_slist (add_unique (unique s) x).
- Definition remove (x : elt)(s : t) : t := Build_slist (remove_unique (unique s) x).
- Definition singleton (x : elt) : t := Build_slist (singleton_unique x).
+ Definition mem (x : elt) (s : t) : bool := Raw.mem x s.
+ Definition add (x : elt)(s : t) : t  := Build_slist (Raw.add_unique (unique s) x).
+ Definition remove (x : elt)(s : t) : t := Build_slist (Raw.remove_unique (unique s) x).
+ Definition singleton (x : elt) : t := Build_slist (Raw.singleton_unique x).
  Definition union (s s' : t) : t :=
-   Build_slist (union_unique (unique s) (unique s')). 
+   Build_slist (Raw.union_unique (unique s) (unique s')). 
  Definition inter (s s' : t) : t :=
-   Build_slist (inter_unique (unique s) (unique s')). 
+   Build_slist (Raw.inter_unique (unique s) (unique s')). 
  Definition diff (s s' : t) : t :=
-   Build_slist (diff_unique (unique s) (unique s')). 
- Definition equal (s s' : t) : bool := equal s s'. 
- Definition subset (s s' : t) : bool := subset s s'.
- Definition empty : t := Build_slist empty_unique.
- Definition is_empty (s : t) : bool := is_empty s.
- Definition elements (s : t) : list elt := elements s.
- Definition choose (s:t) : option elt := choose s.
- Definition fold (B : Set) (f : elt -> B -> B) (s : t) : B -> B := fold (B:=B) f s. 
- Definition cardinal (s : t) : nat := cardinal s.
+   Build_slist (Raw.diff_unique (unique s) (unique s')). 
+ Definition equal (s s' : t) : bool := Raw.equal s s'. 
+ Definition subset (s s' : t) : bool := Raw.subset s s'.
+ Definition empty : t := Build_slist Raw.empty_unique.
+ Definition is_empty (s : t) : bool := Raw.is_empty s.
+ Definition elements (s : t) : list elt := Raw.elements s.
+ Definition choose (s:t) : option elt := Raw.choose s.
+ Definition fold (B : Set) (f : elt -> B -> B) (s : t) : B -> B := Raw.fold (B:=B) f s. 
+ Definition cardinal (s : t) : nat := Raw.cardinal s.
  Definition filter (f : elt -> bool) (s : t) : t :=
-   Build_slist (filter_unique (unique s) f).
- Definition for_all (f : elt -> bool) (s : t) : bool := for_all f s.
- Definition exists_ (f : elt -> bool) (s : t) : bool := exists_ f s.
+   Build_slist (Raw.filter_unique (unique s) f).
+ Definition for_all (f : elt -> bool) (s : t) : bool := Raw.for_all f s.
+ Definition exists_ (f : elt -> bool) (s : t) : bool := Raw.exists_ f s.
  Definition partition (f : elt -> bool) (s : t) : t * t :=
-   let p := partition f s in
-   (Build_slist (this:=fst p) (partition_unique_1 (unique s) f),
-   Build_slist (this:=snd p) (partition_unique_2 (unique s) f)).
+   let p := Raw.partition f s in
+   (Build_slist (this:=fst p) (Raw.partition_unique_1 (unique s) f),
+   Build_slist (this:=snd p) (Raw.partition_unique_2 (unique s) f)).
 
  Section Spec. 
   Variable s s' : t.
   Variable x y : elt.
 
-  Lemma In_1 : X.eq x y -> In x s -> In y s. 
-  Proof. exact (fun H H' => In_eq H H'). Qed.
+  Lemma In_1 : E.eq x y -> In x s -> In y s. 
+  Proof. exact (fun H H' => Raw.In_eq H H'). Qed.
  
   Lemma mem_1 : In x s -> mem x s = true.
-  Proof. exact (fun H => mem_1 H). Qed.
+  Proof. exact (fun H => Raw.mem_1 H). Qed.
   Lemma mem_2 : mem x s = true -> In x s. 
-  Proof. exact (fun H => mem_2 H). Qed.
+  Proof. exact (fun H => Raw.mem_2 H). Qed.
  
   Lemma equal_1 : Equal s s' -> equal s s' = true.
-  Proof. exact (equal_1 s.(unique) s'.(unique)). Qed.
+  Proof. exact (Raw.equal_1 s.(unique) s'.(unique)). Qed.
   Lemma equal_2 : equal s s' = true -> Equal s s'.
-  Proof. exact (equal_2 s.(unique) s'.(unique)). Qed.
+  Proof. exact (Raw.equal_2 s.(unique) s'.(unique)). Qed.
 
   Lemma subset_1 : Subset s s' -> subset s s' = true.
-  Proof. exact (subset_1 s.(unique) s'.(unique)). Qed.
+  Proof. exact (Raw.subset_1 s.(unique) s'.(unique)). Qed.
   Lemma subset_2 : subset s s' = true -> Subset s s'.
-  Proof. exact (subset_2 s.(unique) s'.(unique)). Qed.
+  Proof. exact (Raw.subset_2 s.(unique) s'.(unique)). Qed.
 
   Lemma empty_1 : Empty empty.
-  Proof. exact empty_1. Qed.
+  Proof. exact Raw.empty_1. Qed.
 
   Lemma is_empty_1 : Empty s -> is_empty s = true. 
-  Proof. exact (fun H => is_empty_1 H). Qed.
+  Proof. exact (fun H => Raw.is_empty_1 H). Qed.
   Lemma is_empty_2 : is_empty s = true -> Empty s.
-  Proof. exact (fun H => is_empty_2 H). Qed.
+  Proof. exact (fun H => Raw.is_empty_2 H). Qed.
  
-  Lemma add_1 : X.eq x y -> In y (add x s).
-  Proof. exact (fun H => add_1 s.(unique) H). Qed.
+  Lemma add_1 : E.eq x y -> In y (add x s).
+  Proof. exact (fun H => Raw.add_1 s.(unique) H). Qed.
   Lemma add_2 : In y s -> In y (add x s).
-  Proof. exact (fun H => add_2 s.(unique) x H). Qed.
-  Lemma add_3 : ~ X.eq x y -> In y (add x s) -> In y s. 
-  Proof. exact (fun H => add_3 s.(unique) H). Qed.
-
-  Lemma remove_1 : X.eq x y -> ~ In y (remove x s).
-  Proof. exact (fun H => remove_1 s.(unique) H). Qed.
-  Lemma remove_2 : ~ X.eq x y -> In y s -> In y (remove x s).
-  Proof. exact (fun H H' => remove_2 s.(unique) H H'). Qed.
+  Proof. exact (fun H => Raw.add_2 s.(unique) x H). Qed.
+  Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s. 
+  Proof. exact (fun H => Raw.add_3 s.(unique) H). Qed.
+
+  Lemma remove_1 : E.eq x y -> ~ In y (remove x s).
+  Proof. exact (fun H => Raw.remove_1 s.(unique) H). Qed.
+  Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s).
+  Proof. exact (fun H H' => Raw.remove_2 s.(unique) H H'). Qed.
   Lemma remove_3 : In y (remove x s) -> In y s.
-  Proof. exact (fun H => remove_3 s.(unique) H). Qed.
+  Proof. exact (fun H => Raw.remove_3 s.(unique) H). Qed.
 
-  Lemma singleton_1 : In y (singleton x) -> X.eq x y. 
-  Proof. exact (fun H => singleton_1 H). Qed.
-  Lemma singleton_2 : X.eq x y -> In y (singleton x). 
-  Proof. exact (fun H => singleton_2 H). Qed.
+  Lemma singleton_1 : In y (singleton x) -> E.eq x y. 
+  Proof. exact (fun H => Raw.singleton_1 H). Qed.
+  Lemma singleton_2 : E.eq x y -> In y (singleton x). 
+  Proof. exact (fun H => Raw.singleton_2 H). Qed.
 
   Lemma union_1 : In x (union s s') -> In x s \/ In x s'.
-  Proof. exact (fun H => union_1 s.(unique) s'.(unique) H). Qed.
+  Proof. exact (fun H => Raw.union_1 s.(unique) s'.(unique) H). Qed.
   Lemma union_2 : In x s -> In x (union s s'). 
-  Proof. exact (fun H => union_2 s.(unique) s'.(unique) H). Qed.
+  Proof. exact (fun H => Raw.union_2 s.(unique) s'.(unique) H). Qed.
   Lemma union_3 : In x s' -> In x (union s s').
-  Proof. exact (fun H => union_3 s.(unique) s'.(unique) H). Qed.
+  Proof. exact (fun H => Raw.union_3 s.(unique) s'.(unique) H). Qed.
 
   Lemma inter_1 : In x (inter s s') -> In x s.
-  Proof. exact (fun H => inter_1 s.(unique) s'.(unique) H). Qed.
+  Proof. exact (fun H => Raw.inter_1 s.(unique) s'.(unique) H). Qed.
   Lemma inter_2 : In x (inter s s') -> In x s'.
-  Proof. exact (fun H => inter_2 s.(unique) s'.(unique) H). Qed.
+  Proof. exact (fun H => Raw.inter_2 s.(unique) s'.(unique) H). Qed.
   Lemma inter_3 : In x s -> In x s' -> In x (inter s s').
-  Proof. exact (fun H => inter_3 s.(unique) s'.(unique) H). Qed.
+  Proof. exact (fun H => Raw.inter_3 s.(unique) s'.(unique) H). Qed.
 
   Lemma diff_1 : In x (diff s s') -> In x s. 
-  Proof. exact (fun H => diff_1 s.(unique) s'.(unique) H). Qed.
+  Proof. exact (fun H => Raw.diff_1 s.(unique) s'.(unique) H). Qed.
   Lemma diff_2 : In x (diff s s') -> ~ In x s'.
-  Proof. exact (fun H => diff_2 s.(unique) s'.(unique) H). Qed.
+  Proof. exact (fun H => Raw.diff_2 s.(unique) s'.(unique) H). Qed.
   Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').
-  Proof. exact (fun H => diff_3 s.(unique) s'.(unique) H). Qed.
+  Proof. exact (fun H => Raw.diff_3 s.(unique) s'.(unique) H). Qed.
  
   Lemma fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A),
       fold f s i = fold_left (fun a e => f e a) (elements s) i.
-  Proof. exact (fold_1 s.(unique)). Qed.
+  Proof. exact (Raw.fold_1 s.(unique)). Qed.
 
   Lemma cardinal_1 : cardinal s = length (elements s).
-  Proof. exact (cardinal_1 s.(unique)). Qed.
+  Proof. exact (Raw.cardinal_1 s.(unique)). Qed.
 
   Section Filter.
   
   Variable f : elt -> bool.
 
-  Lemma filter_1 : compat_bool X.eq f -> In x (filter f s) -> In x s. 
-  Proof. exact (fun H => @filter_1 s x f). Qed.
-  Lemma filter_2 : compat_bool X.eq f -> In x (filter f s) -> f x = true. 
-  Proof. exact (@filter_2 s x f). Qed.
+  Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s. 
+  Proof. exact (fun H => @Raw.filter_1 s x f). Qed.
+  Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true. 
+  Proof. exact (@Raw.filter_2 s x f). Qed.
   Lemma filter_3 :
-      compat_bool X.eq f -> In x s -> f x = true -> In x (filter f s).
-  Proof. exact (@filter_3 s x f). Qed.
+      compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
+  Proof. exact (@Raw.filter_3 s x f). Qed.
 
   Lemma for_all_1 :
-      compat_bool X.eq f ->
+      compat_bool E.eq f ->
       For_all (fun x => f x = true) s -> for_all f s = true.
-  Proof. exact (@for_all_1 s f). Qed.
+  Proof. exact (@Raw.for_all_1 s f). Qed.
   Lemma for_all_2 :
-      compat_bool X.eq f ->
+      compat_bool E.eq f ->
       for_all f s = true -> For_all (fun x => f x = true) s.
-  Proof. exact (@for_all_2 s f). Qed.
+  Proof. exact (@Raw.for_all_2 s f). Qed.
 
   Lemma exists_1 :
-      compat_bool X.eq f ->
+      compat_bool E.eq f ->
       Exists (fun x => f x = true) s -> exists_ f s = true.
-  Proof. exact (@exists_1 s f). Qed.
+  Proof. exact (@Raw.exists_1 s f). Qed.
   Lemma exists_2 :
-      compat_bool X.eq f ->
+      compat_bool E.eq f ->
       exists_ f s = true -> Exists (fun x => f x = true) s.
-  Proof. exact (@exists_2 s f). Qed.
+  Proof. exact (@Raw.exists_2 s f). Qed.
 
   Lemma partition_1 :
-      compat_bool X.eq f -> Equal (fst (partition f s)) (filter f s).
-  Proof. exact (@partition_1 s f). Qed.
+      compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s).
+  Proof. exact (@Raw.partition_1 s f). Qed.
   Lemma partition_2 :
-      compat_bool X.eq f ->
+      compat_bool E.eq f ->
       Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
-  Proof. exact (@partition_2 s f). Qed.
+  Proof. exact (@Raw.partition_2 s f). Qed.
 
   End Filter.
 
-  Lemma elements_1 : In x s -> InA X.eq x (elements s).
-  Proof. exact (fun H => elements_1 H). Qed.
-  Lemma elements_2 : InA X.eq x (elements s) -> In x s.
-  Proof. exact (fun H => elements_2 H). Qed.
-  Lemma elements_3 : NoDupA X.eq (elements s).
-  Proof. exact (elements_3 s.(unique)). Qed.
+  Lemma elements_1 : In x s -> InA E.eq x (elements s).
+  Proof. exact (fun H => Raw.elements_1 H). Qed.
+  Lemma elements_2 : InA E.eq x (elements s) -> In x s.
+  Proof. exact (fun H => Raw.elements_2 H). Qed.
+  Lemma elements_3 : NoDupA E.eq (elements s).
+  Proof. exact (Raw.elements_3 s.(unique)). Qed.
 
   Lemma choose_1 : choose s = Some x -> In x s.
-  Proof. exact (fun H => choose_1 H). Qed.
+  Proof. exact (fun H => Raw.choose_1 H). Qed.
   Lemma choose_2 : choose s = None -> Empty s.
-  Proof. exact (fun H => choose_2 H). Qed.
+  Proof. exact (fun H => Raw.choose_2 H). Qed.
 
  End Spec.
 
diff --git a/theories/FSets/OrderedType.v b/theories/FSets/OrderedType.v
index 0268b38c9..d989d8937 100644
--- a/theories/FSets/OrderedType.v
+++ b/theories/FSets/OrderedType.v
@@ -313,6 +313,8 @@ Ltac false_order := elimtype False; order.
 
 (* Specialization of resuts about lists modulo. *)
 
+Section ForNotations.
+
 Notation In:=(InA eq).
 Notation Inf:=(lelistA lt).
 Notation Sort:=(sort lt).
@@ -346,6 +348,8 @@ Proof. exact (InfA_alt eq_refl eq_sym lt_trans lt_eq eq_lt). Qed.
 Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
 Proof. exact (SortA_NoDupA eq_refl eq_sym lt_trans lt_not_eq lt_eq eq_lt) . Qed.
 
+End ForNotations.
+
 Hint Resolve ListIn_In Sort_NoDup Inf_lt. 
 Hint Immediate In_eq Inf_lt.