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

diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v
index 67b20d5d2..24efa44ef 100644
--- a/theories/FSets/FSetToFiniteSet.v
+++ b/theories/FSets/FSetToFiniteSet.v
@@ -20,7 +20,7 @@ Require Import FSetInterface FSetProperties OrderedTypeEx DecidableTypeEx.
     to the good old [Ensembles] and [Finite_sets] theory. *)
 
 Module WS_to_Finite_set (U:UsualDecidableType)(M: WSfun U).
- Module MP:= WProperties U M.
+ Module MP:= WProperties_fun U M.
  Import M MP FM Ensembles Finite_sets.
 
  Definition mkEns : M.t -> Ensemble M.elt := 
@@ -155,9 +155,7 @@ Module WS_to_Finite_set (U:UsualDecidableType)(M: WSfun U).
 End WS_to_Finite_set.
 
 
-Module S_to_Finite_set (U:UsualOrderedType)(M: Sfun U).
-  Module D := OT_as_DT U.
-  Include WS_to_Finite_set D M.
-End S_to_Finite_set.
+Module S_to_Finite_set (U:UsualOrderedType)(M: Sfun U) :=
+  WS_to_Finite_set U M.