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

diff --git a/theories/Logic/DecidableType.v b/theories/Logic/DecidableType.v
index a4de6ca7f..6b3cccae9 100644
--- a/theories/Logic/DecidableType.v
+++ b/theories/Logic/DecidableType.v
@@ -12,6 +12,23 @@ Require Export SetoidList.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+(** * Types with Equalities, and nothing more (for subtyping purpose) *)
+
+Module Type EqualityType. 
+
+  Parameter t : Set.
+
+  Parameter eq : t -> t -> Prop.
+
+  Axiom eq_refl : forall x : t, eq x x.
+  Axiom eq_sym : forall x y : t, eq x y -> eq y x.
+  Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
+
+  Hint Immediate eq_sym.
+  Hint Resolve eq_refl eq_trans.
+
+End EqualityType. 
+
 (** * Types with decidable Equalities (but no ordering) *)
 
 Module Type DecidableType.