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, 7 insertions, 7 deletions

diff --git a/theories/FSets/OrderedType.v b/theories/FSets/OrderedType.v
index d59a9a354..ddee6c289 100644
--- a/theories/FSets/OrderedType.v
+++ b/theories/FSets/OrderedType.v
@@ -12,13 +12,6 @@ Require Export SetoidList.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(* TODO concernant la tactique order: 
-   * propagate_lt n'est sans doute pas complet
-   * un propagate_le
-   * exploiter les hypotheses negatives restant a la fin
-   * faire que ca marche meme quand une hypothese depend d'un eq ou lt.
-*) 
-
 (** * Ordered types *)
 
 Inductive Compare (X : Set) (lt eq : X -> X -> Prop) (x y : X) : Set :=
@@ -122,6 +115,13 @@ Module OrderedTypeFacts (O: OrderedType).
    intuition.
   Qed.
 
+(* TODO concernant la tactique order: 
+   * propagate_lt n'est sans doute pas complet
+   * un propagate_le
+   * exploiter les hypotheses negatives restant a la fin
+   * faire que ca marche meme quand une hypothese depend d'un eq ou lt.
+*) 
+
 Ltac abstraction := match goal with 
  (* First, some obvious simplifications *)
  | H : False |- _ => elim H