Revision of the FSetWeak Interface, so that it becomes a precise

subtype of the FSet Interface (and idem for FMapWeak / FMap). 

1) No eq_dec is officially required in FSetWeakInterface.S.E
(EqualityType instead of DecidableType). But of course,
implementations still needs this eq_dec. 

2) elements_3 differs in FSet and FSetWeak (sort vs. nodup). In
FSetWeak we rename it into elements_3w, whereas in FSet we
artificially add elements_3w along to the original elements_3.

Initial steps toward factorization of FSetFacts and FSetWeakFacts, 
and so on...

Even if it's not required, FSetWeakList provides a eq_dec on sets, 
allowing weak sets of weak sets. 





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

1 files changed, 5 insertions, 7 deletions

diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index d6c978c05..2315dc532 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -29,19 +29,17 @@ Module Properties (M: S).
   Import ME. (* for ME.eq_dec *)
   Import M.E.
   Import M.
+  Module FM := Facts M.
+  Import FM.
   Import Logic. (* to unmask [eq] *)  
   Import Peano. (* to unmask [lt] *)
-  
-   (** Results about lists without duplicates *)
 
-  Module FM := Facts M.
-  Import FM.
+  (** Results about lists without duplicates *)
 
   Definition Add x s s' := forall y, In y s' <-> E.eq x y \/ In y s.
   Definition Above x s := forall y, In y s -> E.lt y x.
   Definition Below x s := forall y, In y s -> E.lt x y.
 
-
   Lemma In_dec : forall x s, {In x s} + {~ In x s}.
   Proof.
   intros; generalize (mem_iff s x); case (mem x s); intuition.
@@ -231,14 +229,14 @@ Module Properties (M: S).
    union (remove x s) (add x s') [=] union (add x s) (remove x s').
   Proof.
   unfold Equal; intros; set_iff.
-  destruct (ME.eq_dec x a); intuition.
+  destruct (eq_dec x a); intuition.
   Qed.
 
   Lemma union_remove_add_2 : In x s -> 
    union (remove x s) (add x s') [=] union s s'.
   Proof.
   unfold Equal; intros; set_iff.
-  destruct (ME.eq_dec x a); intuition.
+  destruct (eq_dec x a); intuition.
   left; eauto with set.
   Qed.