18 files changed, 171 insertions, 139 deletions

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index fc0926b361..4b4d2549fc 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 917534e195..ebc99933b5 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 e2ea687945..a99c6a9089 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 39b214dec3..37cacbc75e 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 6a1e07185a..10e06711f1 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 0fb41931c4..e0e8582111 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 82c684634c..b7a1deb771 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 9d47ef72c1..e5f4bb3c90 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 6afb8fcb7b..8c692bd079 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 5f04e73c61..ac8800923f 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 bc0cf95e18..37f81476d3 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 928083b601..394531bbb9 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 d64cab1732..93a967cdb0 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 67b20d5d2c..24efa44ef9 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 0dfc05689a..8a2f0502aa 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 9f8412a60f..95c9c31a91 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 dbc72e0e7a..8f82fe93dc 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 30a7bb6332..57a2248b36 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.