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

19 files changed, 176 insertions, 139 deletions

diff --git a/CHANGES b/CHANGES
index fbb3b5541..395b4cf70 100644
--- a/CHANGES
+++ b/CHANGES
@@ -116,6 +116,11 @@ Libraries (DOC TO CHECK)
     thanks to new features of Coq modules (in particular Include), see
     FSetInterface. Same for maps. Hints in these interfaces have been
     reworked (they are now placed in a "set" database). 
+  * To allow full subtyping between weak and ordered sets, a field
+    "eq_dec" has been added to OrderedType. The old version of OrderedType
+    is now called MiniOrderedType and functor MOT_to_OT allow to 
+    convert to the new version. The interfaces and implementations
+    of sets now contain also such a "eq_dec" field.
   * FSetDecide, contributed by Aaron Bohannon, contains a decision
     procedure allowing to solve basic set-related goals (for instance, 
     is a point in a particular set ?). See FSetProperties for examples.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index fc0926b36..4b4d2549f 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -22,7 +22,7 @@ Unset Strict Implicit.
 
 (** * Facts about weak maps *)
 
-Module WFacts (E:DecidableType)(Import M:WSfun E).
+Module WFacts_fun (E:DecidableType)(Import M:WSfun E).
 
 Notation eq_dec := E.eq_dec.
 Definition eqb x y := if eq_dec x y then true else false.
@@ -741,22 +741,20 @@ Qed.
 (* old name: *)
 Notation not_find_mapsto_iff := not_find_in_iff.
 
-End WFacts.
+End WFacts_fun.
 
-(** * Same facts for full maps *)
+(** * Same facts for self-contained weak sets and for full maps *)
 
-Module Facts (M:S). 
- Module D := OT_as_DT M.E.
- Include WFacts D M.
-End Facts.
+Module WFacts (M:S) := WFacts_fun M.E M.
+Module Facts := WFacts.
 
 (** * Additional Properties for weak maps 
  
     Results about [fold], [elements], induction principles...
 *)
 
-Module WProperties (E:DecidableType)(M:WSfun E).
- Module Import F:=WFacts E M. 
+Module WProperties_fun (E:DecidableType)(M:WSfun E).
+ Module Import F:=WFacts_fun E M. 
  Import M.
 
  Section Elt. 
@@ -1107,14 +1105,12 @@ Module WProperties (E:DecidableType)(M:WSfun E).
  Add Parametric Morphism elt : (@cardinal elt) with signature Equal ==> @Logic.eq _ as cardinal_m.
  Proof. intros; apply Equal_cardinal; auto. Qed.
 
-End WProperties.
+End WProperties_fun.
 
-(** * Same Properties for full maps *)
+(** * Same Properties for self-contained weak maps and for full maps *)
 
-Module Properties (M:S). 
- Module D := OT_as_DT M.E.
- Include WProperties D M.
-End Properties.
+Module WProperties (M:WS) := WProperties_fun M.E M.
+Module Properties := WProperties.
 
 (** * Properties specific to maps with ordered keys *)
 
@@ -1273,7 +1269,7 @@ Module OrdProperties (M:S).
   rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff.
   rewrite add_mapsto_iff; unfold O.eqke; simpl.
   intuition.
-  destruct (ME.eq_dec x t0); auto.
+  destruct (E.eq_dec x t0); auto.
   elimtype False.
   assert (In t0 m).
    exists e0; auto.
@@ -1303,7 +1299,7 @@ Module OrdProperties (M:S).
   rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff.
   rewrite add_mapsto_iff; unfold O.eqke; simpl.
   intuition.
-  destruct (ME.eq_dec x t0); auto.
+  destruct (E.eq_dec x t0); auto.
   elimtype False.
   assert (In t0 m).
    exists e0; auto.
@@ -1359,7 +1355,7 @@ Module OrdProperties (M:S).
   inversion_clear H1; [ | inversion_clear H2; eauto ].
   red in H3; simpl in H3; destruct H3.
   destruct p as (p1,p2).
-  destruct (ME.eq_dec p1 x).
+  destruct (E.eq_dec p1 x).
   apply ME.lt_eq with p1; auto.
    inversion_clear H2.
    inversion_clear H5.
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index 917534e19..ebc99933b 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -55,11 +55,7 @@ Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true.
     No requirements for an ordering on keys nor elements, only decidability
     of equality on keys. First, a functorial signature: *)
 
-Module Type WSfun (E : EqualityType).
-
-  (** The module E of base objects is meant to be a [DecidableType]
-     (and used to be so). But requiring only an [EqualityType] here
-     allows subtyping between weak and ordered maps. *)
+Module Type WSfun (E : DecidableType).
 
   Definition key := E.t.
 
@@ -261,7 +257,7 @@ End WSfun.
     Similar to [WSfun] but expressed in a self-contained way. *)
 
 Module Type WS. 
-  Declare Module E : EqualityType.
+  Declare Module E : DecidableType.
   Include Type WSfun E.
 End WS.
 
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index e2ea68794..a99c6a908 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -402,7 +402,7 @@ Proof.
  elim (Sort_Inf_NotIn H6 H7).
  destruct H as (e'', hyp); exists e''; auto.
  apply MapsTo_eq with k; auto; order.
- apply H1 with k; destruct (eq_dec x k); auto.
+ apply H1 with k; destruct (X.eq_dec x k); auto.
 
 
  destruct (X.compare x x'); try contradiction; clear y.
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 39b214dec..37cacbc75 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -111,17 +111,17 @@ Module PositiveOrderedTypeBits <: UsualOrderedType.
   apply EQ; red; auto.
   Qed.
 
-End PositiveOrderedTypeBits.
-
-(** Other positive stuff *)
-
-Lemma peq_dec (x y: positive): {x = y} + {x <> y}.
-Proof.
+  Lemma eq_dec (x y: positive): {x = y} + {x <> y}.
+  Proof.
   intros. case_eq ((x ?= y) Eq); intros.
   left. apply Pcompare_Eq_eq; auto.
   right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
   right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
-Qed.
+  Qed.
+
+End PositiveOrderedTypeBits.
+
+(** Other positive stuff *)
  
 Fixpoint append (i j : positive) {struct i} : positive :=
     match i with
@@ -717,7 +717,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Lemma remove_3 : MapsTo y e (remove x m) -> MapsTo y e m.
   Proof. 
   unfold MapsTo.
-  destruct (peq_dec x y).
+  destruct (E.eq_dec x y).
   subst.
   rewrite grs; intros; discriminate.
   rewrite gro; auto.
@@ -1166,10 +1166,10 @@ Module PositiveMapAdditionalFacts.
   (* Derivable from the Map interface *)
   Theorem gsspec:
     forall (A:Type)(i j: positive) (x: A) (m: t A),
-    find i (add j x m) = if peq_dec i j then Some x else find i m.
+    find i (add j x m) = if E.eq_dec i j then Some x else find i m.
   Proof.
     intros.
-    destruct (peq_dec i j); [ rewrite e; apply gss | apply gso; auto ].
+    destruct (E.eq_dec i j); [ rewrite e; apply gss | apply gso; auto ].
   Qed.
 
    (* Not derivable from the Map interface *)
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 6a1e07185..10e06711f 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -1881,6 +1881,14 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
   destruct Raw.compare; intros; [apply EQ|apply LT|apply GT]; red; auto.
  Defined.
 
+ Definition eq_dec (s s':t) : { eq s s' } + { ~ eq s s' }.
+ Proof.
+  intros (s,b) (s',b'); unfold eq; simpl.
+  case_eq (Raw.equal s s'); intro H; [left|right].
+  apply equal_2; auto.
+  intro H'; rewrite equal_1 in H; auto; discriminate.
+ Defined.
+
  (* specs *)
  Section Specs. 
  Variable s s' s'': t. 
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 0fb41931c..e0e858211 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -20,11 +20,8 @@ Set Firstorder Depth 2.
 
 (** * From non-dependent signature [S] to dependent signature [Sdep]. *)
 
-Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
-  Import M.
+Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
 
-  Module ME := OrderedTypeFacts E.
-   
   Definition empty : {s : t | Empty s}.
   Proof. 
     exists empty; auto with set.
@@ -50,7 +47,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
   Proof.
     intros; exists (add x s); auto.
     unfold Add in |- *; intuition.
-    elim (ME.eq_dec x y); auto.
+    elim (E.eq_dec x y); auto.
     intros; right. 
     eapply add_3; eauto.
   Qed. 
@@ -68,7 +65,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
     intros; exists (remove x s); intuition.
     absurd (In x (remove x s)); auto with set.
     apply In_1 with y; auto. 
-    elim (ME.eq_dec x y); intros; auto.
+    elim (E.eq_dec x y); intros; auto.
     absurd (In x (remove x s)); auto with set.
     apply In_1 with y; auto. 
     eauto with set.
@@ -396,6 +393,8 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
     intros; discriminate H.
   Qed.
 
+  Definition eq_dec := equal.
+
   Definition equal (s s' : t) : bool :=
     if equal s s' then true else false.
 
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 82c684634..b7a1deb77 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -19,10 +19,10 @@
 
 Require Import Decidable DecidableTypeEx FSetFacts.
 
-(** First, a version for Weak Sets *)
+(** First, a version for Weak Sets in functorial presentation *)
 
-Module WDecide (E : DecidableType)(Import M : WSfun E).
- Module F := FSetFacts.WFacts E M.
+Module WDecide_fun (E : DecidableType)(Import M : WSfun E).
+ Module F := FSetFacts.WFacts_fun E M.
 
 (** * Overview
     This functor defines the tactic [fsetdec], which will
@@ -851,15 +851,14 @@ the above form:
 
   End FSetDecideTestCases.
 
-End WDecide.
+End WDecide_fun.
 
 Require Import FSetInterface.
 
-(** Now comes a special version dedicated to full sets. For this 
-    one, only one argument [(M:S)] is necessary. *)
+(** 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 [Decide] functor which is meant to be
+    used on modules [(M:S)] can simply be an alias of [WDecide]. *)
 
-Module Decide (M : S).
-  Module D:=OT_as_DT M.E.
-  Module WD := WDecide D M.
-  Ltac fsetdec := WD.fsetdec.
-End Decide.
\ No newline at end of file
+Module WDecide (M:WS) := WDecide_fun M.E M.
+Module Decide := WDecide.
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.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 6afb8fcb7..8c692bd07 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -21,11 +21,9 @@ Require Export FSetInterface.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** 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 WFacts (Import E : DecidableType)(Import M : WSfun E).
+Module WFacts_fun (Import E : DecidableType)(Import M : WSfun E).
 
 Notation eq_dec := E.eq_dec.
 Definition eqb x y := if eq_dec x y then true else false.
@@ -491,15 +489,14 @@ Qed.
 Add Morphism cardinal ; cardinal_m.
 *)
 
-End WFacts.
+End WFacts_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 [Facts] functor which is meant to be
+    used on modules [(M:S)] can simply be an alias of [WFacts]. *)
 
-(** Now comes a special version dedicated to full sets. For this 
-    one, only one argument [(M:S)] is necessary. *)
+Module WFacts (M:WS) := WFacts_fun M.E M.
+Module Facts := WFacts.
 
-Module Facts (Import M:S).
-  Module D:=OT_as_DT M.E.
-  Include WFacts D M.
-
-End Facts.
 
diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v
index 5f04e73c6..ac8800923 100644
--- a/theories/FSets/FSetFullAVL.v
+++ b/theories/FSets/FSetFullAVL.v
@@ -913,6 +913,14 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
   change (Raw.Equal s s'); auto.
  Defined.
 
+ Definition eq_dec (s s':t) : { eq s s' } + { ~ eq s s' }.
+ Proof.
+  intros (s,b,a) (s',b',a'); unfold eq; simpl.
+  case_eq (Raw.equal s s'); intro H; [left|right].
+  apply equal_2; auto.
+  intro H'; rewrite equal_1 in H; auto; discriminate.
+ Defined.
+
  (* specs *)
  Section Specs. 
  Variable s s' s'': t. 
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index bc0cf95e1..37f81476d 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -44,11 +44,7 @@ Unset Strict Implicit.
     Weak sets are sets without ordering on base elements, only 
     a decidable equality. *)
 
-Module Type WSfun (E : EqualityType).
-
-  (** The module E of base objects is meant to be a [DecidableType]
-     (and used to be so). But requiring only an [EqualityType] here
-     allows subtyping between weak and ordered sets *)
+Module Type WSfun (E : DecidableType).
 
   Definition elt := E.t.
 
@@ -95,12 +91,8 @@ Module Type WSfun (E : EqualityType).
   (** Set difference. *)
 
   Definition eq : t -> t -> Prop := Equal.
-  (** In order to have the subtyping WS < S between weak and ordered 
-   sets, we do not require here an [eq_dec]. This interface is hence 
-   not compatible with [DecidableType], but only with [EqualityType],
-   so in general it may not possible to form weak sets of weak sets.
-   Some particular implementations may allow this nonetheless, in 
-   particular [FSetWeakList.Make]. *)
+
+  Parameter eq_dec : forall s s', { eq s s' } + { ~ eq s s' }.
 
   Parameter equal : t -> t -> bool.
   (** [equal s1 s2] tests whether the sets [s1] and [s2] are
@@ -282,7 +274,7 @@ End WSfun.
     module [E] of base elements is incorporated in the signature. *)
 
 Module Type WS.
-  Declare Module E : EqualityType.
+  Declare Module E : DecidableType.
   Include Type WSfun E.
 End WS.
 
@@ -367,17 +359,16 @@ WSfun ---> WS
  |         |
  |         |
  V         V
-Sfun  ---> S 
-
+Sfun  ---> S
 
-Module S_WS (M : S) <: SW := M.
+Module S_WS (M : S) <: WS := M.
 Module Sfun_WSfun (E:OrderedType)(M : Sfun E) <: WSfun E := M.
-Module S_Sfun (E:OrderedType)(M : S with Module E:=E) <: Sfun E := M.
-Module WS_WSfun (E:EqualityType)(M : WS with Module E:=E) <: WSfun E := M.
+Module S_Sfun (M : S) <: Sfun M.E := M.
+Module WS_WSfun (M : WS) <: WSfun M.E := M.
 >>
 *)
 
-(** * Dependent signature 
+(** * Dependent signature
 
     Signature [Sdep] presents ordered sets using dependent types *)
 
@@ -402,7 +393,7 @@ Module Type Sdep.
   Parameter lt : t -> t -> Prop.
   Parameter compare : forall s s' : t, Compare lt eq s s'.
 
-  Parameter eq_refl : forall s : t, eq s s. 
+  Parameter eq_refl : forall s : t, eq s s.
   Parameter eq_sym : forall s s' : t, eq s s' -> eq s' s.
   Parameter eq_trans : forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''.
   Parameter lt_trans : forall s s' s'' : t, lt s s' -> lt s' s'' -> lt s s''.
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index 928083b60..394531bbb 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -1263,6 +1263,14 @@ Module Make (X: OrderedType) <: S with Module E := X.
    auto. 
   Defined.
 
+  Definition eq_dec : { eq s s' } + { ~ eq s s' }.
+  Proof.
+  change eq with Equal.
+  case_eq (equal s s'); intro H; [left | right].
+  apply equal_2; auto.
+  intro H'; rewrite equal_1 in H; auto; discriminate.
+  Qed.
+
  End Spec.
 
 End Make.
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).
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.
 
 
diff --git a/theories/FSets/OrderedType.v b/theories/FSets/OrderedType.v
index 0dfc05689..8a2f0502a 100644
--- a/theories/FSets/OrderedType.v
+++ b/theories/FSets/OrderedType.v
@@ -19,7 +19,7 @@ Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type :=
   | EQ : eq x y -> Compare lt eq x y
   | GT : lt y x -> Compare lt eq x y.
 
-Module Type OrderedType.
+Module Type MiniOrderedType.
 
   Parameter Inline t : Type.
 
@@ -29,7 +29,7 @@ Module Type OrderedType.
   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.
- 
+
   Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
   Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
 
@@ -38,15 +38,34 @@ Module Type OrderedType.
   Hint Immediate eq_sym.
   Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
 
+End MiniOrderedType.
+
+Module Type OrderedType.
+  Include Type MiniOrderedType.
+
+  (** A [eq_dec] can be deduced from [compare] below. But adding this
+     redundant field allows to see an OrderedType as a DecidableType. *)
+  Parameter eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+
 End OrderedType.
 
+Module MOT_to_OT (Import O : MiniOrderedType) <: OrderedType.
+  Include O.
+
+  Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
+  Proof.
+   intros; elim (compare x y); intro H; [ right | left | right ]; auto.
+   assert (~ eq y x); auto.
+  Defined.
+
+End MOT_to_OT.
+
 (** * Ordered types properties *)
 
 (** Additional properties that can be derived from signature
     [OrderedType]. *)
 
-Module OrderedTypeFacts (O: OrderedType). 
-  Import O.
+Module OrderedTypeFacts (Import O: OrderedType).
 
   Lemma lt_antirefl : forall x, ~ lt x x.
   Proof.
@@ -292,11 +311,6 @@ Ltac false_order := elimtype False; order.
   Ltac elim_comp_gt x y :=
     elim (elim_compare_gt (x:=x) (y:=y));
      [ intros _1 _2; rewrite _2; clear _1 _2 | auto ].
-
-  Lemma eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
-  Proof.
-   intros; elim (compare x y); [ right | left | right ]; auto.
-  Defined.
  
   Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}.
   Proof.
diff --git a/theories/FSets/OrderedTypeAlt.v b/theories/FSets/OrderedTypeAlt.v
index 9f8412a60..95c9c31a9 100644
--- a/theories/FSets/OrderedTypeAlt.v
+++ b/theories/FSets/OrderedTypeAlt.v
@@ -15,7 +15,8 @@
 
 Require Import OrderedType.
 
-(** * An alternative (but equivalent) presentation for an Ordered Type inferface. *)
+(** * An alternative (but equivalent) presentation for an Ordered Type
+   inferface. *)
 
 (** NB: [comparison], defined in [Datatypes.v] is [Eq|Lt|Gt]
 whereas [compare], defined in [OrderedType.v] is [EQ _ | LT _ | GT _ ] 
@@ -81,6 +82,12 @@ Module OrderedType_from_Alt (O:OrderedTypeAlt) <: OrderedType.
  rewrite compare_sym; rewrite H; auto.
  Defined.
 
+ Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+ Proof.
+ intros; unfold eq.
+ case (x ?= y); [ left | right | right ]; auto; discriminate.
+ Defined.
+
 End OrderedType_from_Alt. 
 
 (** From the original presentation to this alternative one. *)
diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v
index dbc72e0e7..8f82fe93d 100644
--- a/theories/FSets/OrderedTypeEx.v
+++ b/theories/FSets/OrderedTypeEx.v
@@ -34,6 +34,7 @@ Module Type UsualOrderedType.
  Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
  Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
  Parameter compare : forall x y : t, Compare lt eq x y.
+ Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
 End UsualOrderedType.
 
 (** a [UsualOrderedType] is in particular an [OrderedType]. *)
@@ -68,6 +69,8 @@ Module Nat_as_OT <: UsualOrderedType.
     intro; constructor 3; auto.
   Defined.
 
+  Definition eq_dec := eq_nat_dec.
+
 End Nat_as_OT.
 
 
@@ -99,6 +102,8 @@ Module Z_as_OT <: UsualOrderedType.
     apply GT; unfold lt, Zlt; rewrite <- Zcompare_Gt_Lt_antisym; auto.
   Defined.
 
+  Definition eq_dec := Z_eq_dec.
+
 End Z_as_OT.
 
 (** [positive] is an ordered type with respect to the usual order on natural numbers. *) 
@@ -140,6 +145,11 @@ Module Positive_as_OT <: UsualOrderedType.
   rewrite <- Pcompare_antisym; rewrite H; auto.
   Defined.
 
+  Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+  Proof.
+   intros; unfold eq; decide equality.
+  Defined.
+
 End Positive_as_OT.
 
 
@@ -183,6 +193,11 @@ Module N_as_OT <: UsualOrderedType.
    destruct (Nleb x y); intuition.
   Defined.
 
+  Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+  Proof.
+   intros. unfold eq. decide equality. apply Positive_as_OT.eq_dec.
+  Defined.
+
 End N_as_OT.
 
 
@@ -243,5 +258,12 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
  apply GT; unfold lt; auto.
  Defined.
 
+ Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
+ Proof.
+ intros; elim (compare x y); intro H; [ right | left | right ]; auto.
+ auto using lt_not_eq.
+ assert (~ eq y x); auto using lt_not_eq, eq_sym.
+ Defined.
+
 End PairOrderedType.
 
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.