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

diff --git a/theories/Logic/DecidableTypeEx.v b/theories/Logic/DecidableTypeEx.v
index 30a7bb633..57a2248b3 100644
--- a/theories/Logic/DecidableTypeEx.v
+++ b/theories/Logic/DecidableTypeEx.v
@@ -46,24 +46,16 @@ Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType.
  Definition eq_dec := M.eq_dec.
 End Make_UDT.
 
-(** An OrderedType can be seen as a DecidableType *)
-
-Module OT_as_DT (O:OrderedType) <: DecidableType. 
- Module OF := OrderedTypeFacts O.
- Definition t := O.t.
- Definition eq := O.eq. 
- Definition eq_refl := O.eq_refl. 
- Definition eq_sym := O.eq_sym. 
- Definition eq_trans := O.eq_trans. 
- Definition eq_dec := OF.eq_dec. 
-End OT_as_DT.
+(** An OrderedType can now directly be seen as a DecidableType *)
+
+Module OT_as_DT (O:OrderedType) <: DecidableType := O.
 
 (** (Usual) Decidable Type for [nat], [positive], [N], [Z] *)
 
-Module Nat_as_DT <: UsualDecidableType := OT_as_DT (Nat_as_OT).
-Module Positive_as_DT <: UsualDecidableType := OT_as_DT (Positive_as_OT).
-Module N_as_DT <: UsualDecidableType := OT_as_DT (N_as_OT).
-Module Z_as_DT <: UsualDecidableType := OT_as_DT (Z_as_OT).
+Module Nat_as_DT <: UsualDecidableType := Nat_as_OT.
+Module Positive_as_DT <: UsualDecidableType := Positive_as_OT.
+Module N_as_DT <: UsualDecidableType := N_as_OT.
+Module Z_as_DT <: UsualDecidableType := Z_as_OT.
 
 (** From two decidable types, we can build a new DecidableType 
    over their cartesian product. *)
@@ -99,7 +91,7 @@ End PairDecidableType.
 
 (** Similarly for pairs of UsualDecidableType *)
 
-Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: DecidableType.
+Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
  Definition t := prod D1.t D2.t.
  Definition eq := @eq t.
  Definition eq_refl := @refl_equal t.