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

diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 9d47ef72c..e5f4bb3c9 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -19,8 +19,8 @@
 
 Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx.
 
-Module WEqProperties (Import E:DecidableType)(M:WSfun E). 
-Module Import MP := WProperties E M.
+Module WEqProperties_fun (Import E:DecidableType)(M:WSfun E).
+Module Import MP := WProperties_fun E M.
 Import FM Dec.F.
 Import M.
 
@@ -281,7 +281,7 @@ Qed.
 Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.
 Proof.
 intros; rewrite singleton_b.
-unfold eqb; destruct (eq_dec x y); intuition.
+unfold eqb; destruct (E.eq_dec x y); intuition.
 Qed.
 
 Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.
@@ -927,13 +927,12 @@ Qed.
 
 End Sum.
 
-End WEqProperties.
+End WEqProperties_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 [EqProperties] functor which is meant to be
+    used on modules [(M:S)] can simply be an alias of [WEqProperties]. *)
 
-(** Now comes a special version dedicated to full sets. For this
-    one, only one argument [(M:S)] is necessary. *)
-
-Module EqProperties (M:S).
-  Module D := OT_as_DT M.E.
-  Include WEqProperties D M.
-End EqProperties.
+Module WEqProperties (M:WS) := WEqProperties_fun M.E M.
+Module EqProperties := WEqProperties.