FSet/OrderedType now includes an eq_dec, and hence become an extension of DecidableType

 After lots of hesitations, OrderedType now requires this "eq_dec" field, which
 is redundant (can be deduced from "compare"), but allows the subtyping relation
 DecidableType <= OrderedType, and hence WS <= S : ordered sets are now truly
 extensions of weak sets. Of course this change introduces a last-minute
 incompatibility, but:

  - There is a clear gain in term of functionnality / simplicity.
  - FSets 8.2 already needs some adaptations when compared with 8.1, so it's
    the right time to push such incompatible changes.
  - Transition shouldn't be too hard: the old OrderedType still exists under
    the name MiniOrderedType, and functor MOT_to_OT allows to convert from
    one to the other.

 Beware, for a FSetInterface.WS (resp. S) to be coercible to a DecidableType
 (resp. OrderedType), an eq_dec on sets is now required in these interfaces
 and in the implementations. In pratice, it is really easy to build from
 equal and equal_1 and equal_2.

 Some name changes : in FSetFacts, old WFacts now correspond to WFacts_fun,
 while WFacts now expects only one argument (WFacts M := WFacts_fun M.E M).
 Idem with WDecide, WProperties and WEqProperties.

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

1 files changed, 12 insertions, 14 deletions

diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index d64cab173..93a967cdb 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -24,13 +24,11 @@ Unset Strict Implicit.
 Hint Unfold transpose compat_op.
 Hint Extern 1 (Setoid_Theory _ _) => constructor; congruence.
 
-(** First, a functor for Weak Sets. Since the signature [WS] includes
-    an EqualityType and not a stronger DecidableType, this functor
-    should take two arguments in order to compensate this. *)
+(** First, a functor for Weak Sets in functorial version. *)
 
-Module WProperties (Import E : DecidableType)(M : WSfun E).
-  Module Import Dec := WDecide E M.
-  Module Import FM := Dec.F (* FSetFacts.WFacts E M *).
+Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
+  Module Import Dec := WDecide_fun E M.
+  Module Import FM := Dec.F (* FSetFacts.WFacts_fun E M *).
   Import M.
 
   Lemma In_dec : forall x s, {In x s} + {~ In x s}.
@@ -773,18 +771,18 @@ Module WProperties (Import E : DecidableType)(M : WSfun E).
 
   Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2.
 
-End WProperties.
+End WProperties_fun.
 
+(** Now comes variants for self-contained weak sets and for full sets.
+    For these variants, only one argument is necessary. Thanks to
+    the subtyping [WS<=S], the [Properties] functor which is meant to be
+    used on modules [(M:S)] can simply be an alias of [WProperties]. *)
 
-(** A clone of [WProperties] working on full sets. *)
+Module WProperties (M:WS) := WProperties_fun M.E M.
+Module Properties := WProperties.
 
-Module Properties (M:S).
-  Module D := OT_as_DT M.E.
-  Include WProperties D M.
-End Properties.
 
-
-(** Now comes some properties specific to the element ordering, 
+(** Now comes some properties specific to the element ordering,
     invalid for Weak Sets. *)
 
 Module OrdProperties (M:S).