Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*

 Old stuff DecidableType.v and OrderedType.v stay there and keep their
 names for the moment, for compatibility.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12641 85f007b7-540e-0410-9357-904b9bb8a0f7

37 files changed, 125 insertions, 149 deletions

diff --git a/theories/Arith/MinMax.v b/theories/Arith/MinMax.v
index 32afba489c..6e86a88c59 100644
--- a/theories/Arith/MinMax.v
+++ b/theories/Arith/MinMax.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import OrderedType2 NatOrderedType GenericMinMax.
+Require Import Orders NatOrderedType GenericMinMax.
 
 (** * Maximum and Minimum of two natural numbers *)
 
diff --git a/theories/Arith/NatOrderedType.v b/theories/Arith/NatOrderedType.v
index d9b2b30f04..fa4b7172ad 100644
--- a/theories/Arith/NatOrderedType.v
+++ b/theories/Arith/NatOrderedType.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 Require Import Lt Peano_dec Compare_dec EqNat
- DecidableType2 OrderedType2 OrderTac.
+ Equalities Orders OrdersTac.
 
 
 (** * DecidableType structure for Peano numbers *)
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index e2953f3334..bc6c731f62 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -41,10 +41,10 @@ Unset Strict Implicit.
 (** This is just a compatibility layer, the real implementation
     is now in [MSetAVL] *)
 
-Require FSetCompat MSetAVL OrderedType2 OrderedType2Alt.
+Require FSetCompat MSetAVL Orders OrdersAlt.
 
 Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
- Module X' := OrderedType2Alt.Update_OT X.
+ Module X' := OrdersAlt.Update_OT X.
  Module MSet := MSetAVL.IntMake I X'.
  Include FSetCompat.Backport_Sets X MSet.
 End IntMake.
diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v
index 4a341328ea..971daa2152 100644
--- a/theories/FSets/FSetCompat.v
+++ b/theories/FSets/FSetCompat.v
@@ -221,7 +221,7 @@ End Backport_Sets.
 (** * From old Weak Sets to new ones. *)
 
 Module Update_WSets
- (E:DecidableType2.DecidableType)
+ (E:Equalities.DecidableType)
  (M:FSetInterface.WS with Definition E.t := E.t
                      with Definition E.eq := E.eq)
  <: MSetInterface.WSetsOn E.
@@ -342,7 +342,7 @@ End Update_WSets.
 (** * From old Sets to new ones. *)
 
 Module Update_Sets
- (E:OrderedType2.OrderedType)
+ (E:Orders.OrderedType)
  (M:FSetInterface.S with Definition E.t := E.t
                     with Definition E.eq := E.eq
                     with Definition E.lt := E.lt)
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index 950f48a903..f83259c447 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -20,10 +20,10 @@ Unset Strict Implicit.
 (** This is just a compatibility layer, the real implementation
     is now in [MSetList] *)
 
-Require FSetCompat MSetList OrderedType2 OrderedType2Alt.
+Require FSetCompat MSetList Orders OrdersAlt.
 
 Module Make (X: OrderedType) <: S with Module E := X.
- Module X' := OrderedType2Alt.Update_OT X.
+ Module X' := OrdersAlt.Update_OT X.
  Module MSet := MSetList.Make X'.
  Include FSetCompat.Backport_Sets X MSet.
 End Make.
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 6bf4ae989e..711cbd9a68 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -20,11 +20,11 @@ Unset Strict Implicit.
 (** This is just a compatibility layer, the real implementation
     is now in [MSetWeakList] *)
 
-Require DecidableType2 FSetCompat MSetWeakList.
+Require Equalities FSetCompat MSetWeakList.
 
 Module Make (X: DecidableType) <: WS with Module E := X.
  Module E := X.
- Module X' := DecidableType2.Update_DT X.
+ Module X' := Equalities.Update_DT X.
  Module MSet := MSetWeakList.Make X'.
  Include FSetCompat.Backport_WSets X MSet.
 End Make.
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index cb18785e6c..0de28d5e88 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -30,7 +30,7 @@
 *)
 
 Require Export Bool SetoidList RelationClasses Morphisms
- RelationPairs DecidableType2 OrderedType2 OrderedType2Facts.
+ RelationPairs Equalities Orders OrdersFacts.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index 4292eb9386..b0caf6692f 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -13,7 +13,7 @@
 (** This file proposes an implementation of the non-dependant
     interface [MSetInterface.S] using strictly ordered list. *)
 
-Require Export MSetInterface OrderedType2Facts OrderedType2Lists.
+Require Export MSetInterface OrdersFacts OrdersLists.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v
index dc82a14502..a9ba0a823b 100644
--- a/theories/MSets/MSetProperties.v
+++ b/theories/MSets/MSetProperties.v
@@ -17,7 +17,7 @@
     [Equal s s'] instead of [equal s s'=true], etc. *)
 
 Require Export MSetInterface.
-Require Import DecidableTypeEx OrderedType2Lists MSetFacts MSetDecide.
+Require Import DecidableTypeEx OrdersLists MSetFacts MSetDecide.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/theories/MSets/MSetToFiniteSet.v b/theories/MSets/MSetToFiniteSet.v
index f805a3c965..f0b964cf2d 100644
--- a/theories/MSets/MSetToFiniteSet.v
+++ b/theories/MSets/MSetToFiniteSet.v
@@ -11,7 +11,7 @@
 (** * Finite sets library : conversion to old [Finite_sets] *)
 
 Require Import Ensembles Finite_sets.
-Require Import MSetInterface MSetProperties OrderedType2Ex DecidableType2Ex.
+Require Import MSetInterface MSetProperties OrdersEx.
 
 (** * Going from [MSets] with usual Leibniz equality
     to the good old [Ensembles] and [Finite_sets] theory. *)
diff --git a/theories/MSets/MSets.v b/theories/MSets/MSets.v
index 42966c7fc2..558b09562d 100644
--- a/theories/MSets/MSets.v
+++ b/theories/MSets/MSets.v
@@ -8,11 +8,10 @@
 
 (* $Id$ *)
 
-Require Export OrderedType2.
-Require Export OrderedType2Ex.
-Require Export OrderedType2Alt.
-Require Export DecidableType2.
-Require Export DecidableType2Ex.
+Require Export Orders.
+Require Export OrdersEx.
+Require Export OrdersAlt.
+Require Export Equalities.
 Require Export MSetInterface.
 Require Export MSetFacts.
 Require Export MSetDecide.
diff --git a/theories/NArith/NOrderedType.v b/theories/NArith/NOrderedType.v
index 06db5fa1ce..c5dd395bb2 100644
--- a/theories/NArith/NOrderedType.v
+++ b/theories/NArith/NOrderedType.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import BinNat DecidableType2 OrderedType2 OrderTac.
+Require Import BinNat Equalities Orders OrdersTac.
 
 Local Open Scope N_scope.
 
diff --git a/theories/NArith/Nminmax.v b/theories/NArith/Nminmax.v
index 625fcce237..475b4dfb82 100644
--- a/theories/NArith/Nminmax.v
+++ b/theories/NArith/Nminmax.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import OrderedType2 BinNat Nnat NOrderedType GenericMinMax.
+Require Import Orders BinNat Nnat NOrderedType GenericMinMax.
 
 (** * Maximum and Minimum of two [N] numbers *)
 
diff --git a/theories/NArith/POrderedType.v b/theories/NArith/POrderedType.v
index 041a3a01be..9c0f826185 100644
--- a/theories/NArith/POrderedType.v
+++ b/theories/NArith/POrderedType.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import BinPos DecidableType2 OrderedType2 OrderTac.
+Require Import BinPos Equalities Orders OrdersTac.
 
 Local Open Scope positive_scope.
 
diff --git a/theories/NArith/Pminmax.v b/theories/NArith/Pminmax.v
index 3b3c58841b..4cc48af66e 100644
--- a/theories/NArith/Pminmax.v
+++ b/theories/NArith/Pminmax.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import OrderedType2 BinPos Pnat POrderedType GenericMinMax.
+Require Import Orders BinPos Pnat POrderedType GenericMinMax.
 
 (** * Maximum and Minimum of two positive numbers *)
 
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 5b4e16cafe..480314f96f 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -10,7 +10,7 @@
 
 (*i $Id$ i*)
 
-Require Export DecidableType2 OrderedType2 NumPrelude GenericMinMax.
+Require Export Equalities Orders NumPrelude GenericMinMax.
 
 (** Axiomatization of a domain with zero, successor, predecessor,
     and a bi-directional induction principle. We require [P (S n) = n]
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 6a086f3bd6..9764d15576 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -10,7 +10,7 @@
 
 (*i $Id$ i*)
 
-Require Import NZAxioms NZBase Decidable OrderTac.
+Require Import NZAxioms NZBase Decidable OrdersTac.
 
 Module Type NZOrderPropSig
  (Import NZ : NZOrdSig')(Import NZBase : NZBasePropSig NZ).
diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v
index 74770d6e11..f3229d7236 100644
--- a/theories/QArith/QOrderedType.v
+++ b/theories/QArith/QOrderedType.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import QArith_base DecidableType2 OrderedType2 OrderTac.
+Require Import QArith_base Equalities Orders OrdersTac.
 
 Local Open Scope Q_scope.
 
diff --git a/theories/QArith/Qminmax.v b/theories/QArith/Qminmax.v
index ae9cc46052..d20396c86a 100644
--- a/theories/QArith/Qminmax.v
+++ b/theories/QArith/Qminmax.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import QArith_base OrderedType2 QOrderedType GenericMinMax.
+Require Import QArith_base Orders QOrderedType GenericMinMax.
 
 (** * Maximum and Minimum of two rational numbers *)
 
diff --git a/theories/Reals/ROrderedType.v b/theories/Reals/ROrderedType.v
index ea20db99fb..2b302386ed 100644
--- a/theories/Reals/ROrderedType.v
+++ b/theories/Reals/ROrderedType.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Rbase DecidableType2 OrderedType2 OrderTac.
+Require Import Rbase Equalities Orders OrdersTac.
 
 Local Open Scope R_scope.
 
diff --git a/theories/Reals/Rminmax.v b/theories/Reals/Rminmax.v
index 79343ee45c..373f30ddee 100644
--- a/theories/Reals/Rminmax.v
+++ b/theories/Reals/Rminmax.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import OrderedType2 Rbase Rbasic_fun ROrderedType GenericMinMax.
+Require Import Orders Rbase Rbasic_fun ROrderedType GenericMinMax.
 
 (** * Maximum and Minimum of two real numbers *)
 
diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
index de7a20d4c5..2c72e30b16 100644
--- a/theories/Structures/DecidableType.v
+++ b/theories/Structures/DecidableType.v
@@ -9,19 +9,21 @@
 (* $Id$ *)
 
 Require Export SetoidList.
-Require DecidableType2. (* No Import here, this is on purpose. *)
+Require Equalities.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+(** NB: This file is here only for compatibility with earlier version of
+    [FSets] and [FMap]. Please use [Structures/Equalities.v] directly now. *)
 
 (** * Types with Equalities, and nothing more (for subtyping purpose) *)
 
-Module Type EqualityType := DecidableType2.EqualityTypeOrig.
+Module Type EqualityType := Equalities.EqualityTypeOrig.
 
 (** * Types with decidable Equalities (but no ordering) *)
 
-Module Type DecidableType := DecidableType2.DecidableTypeOrig.
+Module Type DecidableType := Equalities.DecidableTypeOrig.
 
 (** * Additional notions about keys and datas used in FMap *)
 
diff --git a/theories/Structures/DecidableType2Ex.v b/theories/Structures/DecidableType2Ex.v
deleted file mode 100644
index 2ce2b56623..0000000000
--- a/theories/Structures/DecidableType2Ex.v
+++ /dev/null
@@ -1,53 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-Require Import DecidableType2 Morphisms RelationPairs.
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-(** * Examples of Decidable Type structures. *)
-
-
-(** From two decidable types, we can build a new DecidableType
-   over their cartesian product. *)
-
-Module PairDecidableType(D1 D2:DecidableType) <: DecidableType.
-
- Definition t := (D1.t * D2.t)%type.
-
- Definition eq := (D1.eq * D2.eq)%signature.
-
- Instance eq_equiv : Equivalence eq.
-
- Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
- Proof.
- intros (x1,x2) (y1,y2); unfold eq; simpl.
- destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
-  compute; intuition.
- Defined.
-
-End PairDecidableType.
-
-(** Similarly for pairs of UsualDecidableType *)
-
-Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
- Definition t := (D1.t * D2.t)%type.
- Definition eq := @eq t.
- Program Instance eq_equiv : Equivalence eq.
- Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
- Proof.
- intros (x1,x2) (y1,y2);
- destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
- unfold eq, D1.eq, D2.eq in *; simpl;
- (left; f_equal; auto; fail) ||
- (right; intro H; injection H; auto).
- Defined.
-
-End PairUsualDecidableType.
diff --git a/theories/Structures/DecidableTypeEx.v b/theories/Structures/DecidableTypeEx.v
index 022102f70d..4407ead416 100644
--- a/theories/Structures/DecidableTypeEx.v
+++ b/theories/Structures/DecidableTypeEx.v
@@ -12,19 +12,15 @@ Require Import DecidableType OrderedType OrderedTypeEx.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+(** NB: This file is here only for compatibility with earlier version of
+    [FSets] and [FMap]. Please use [Structures/Equalities.v] directly now. *)
+
 (** * Examples of Decidable Type structures. *)
 
 (** A particular case of [DecidableType] where
     the equality is the usual one of Coq. *)
 
-Module Type UsualDecidableType.
- Parameter Inline t : Type.
- Definition eq := @eq t.
- Definition eq_refl := @refl_equal t.
- Definition eq_sym := @sym_eq t.
- Definition eq_trans := @trans_eq t.
- Parameter eq_dec : forall x y, { eq x y }+{~eq x y }.
-End UsualDecidableType.
+Module Type UsualDecidableType := Equalities.UsualDecidableTypeOrig.
 
 (** a [UsualDecidableType] is in particular an [DecidableType]. *)
 
@@ -32,19 +28,10 @@ Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U.
 
 (** an shortcut for easily building a UsualDecidableType *)
 
-Module Type MiniDecidableType.
- Parameter Inline t : Type.
- Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }.
-End MiniDecidableType.
+Module Type MiniDecidableType := Equalities.MiniDecidableType.
 
-Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType.
- Definition t:=M.t.
- Definition eq := @eq t.
- Definition eq_refl := @refl_equal t.
- Definition eq_sym := @sym_eq t.
- Definition eq_trans := @trans_eq t.
- Definition eq_dec := M.eq_dec.
-End Make_UDT.
+Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType
+ := Equalities.Make_UDT M.
 
 (** An OrderedType can now directly be seen as a DecidableType *)
 
diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/Equalities.v
index 2679d25b01..76f539764a 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/Equalities.v
@@ -168,47 +168,49 @@ Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType
    A particular case of [DecidableType] where the equality is
    the usual one of Coq. *)
 
-Module Type UsualEq <: Eq.
- Parameter Inline t : Type.
- Definition eq := @eq t.
-End UsualEq.
+Module Type HasUsualEq (Import T:Typ) <: HasEq T.
+ Definition eq := @Logic.eq t.
+End HasUsualEq.
 
-Module UsualIsEq (E:UsualEq) <: IsEq E.
+Module Type UsualEq <: Eq := Typ <+ HasUsualEq.
+
+Module Type UsualIsEq (E:UsualEq) <: IsEq E.
  Program Instance eq_equiv : Equivalence E.eq.
 End UsualIsEq.
 
-Module UsualIsEqOrig (E:UsualEq) <: IsEqOrig E.
- Definition eq_refl := @eq_refl E.t.
- Definition eq_sym := @eq_sym E.t.
- Definition eq_trans := @eq_trans E.t.
+Module Type UsualIsEqOrig (E:UsualEq) <: IsEqOrig E.
+ Definition eq_refl := @Logic.eq_refl E.t.
+ Definition eq_sym := @Logic.eq_sym E.t.
+ Definition eq_trans := @Logic.eq_trans E.t.
 End UsualIsEqOrig.
 
 Module Type UsualEqualityType <: EqualityType
- := UsualEq <+ IsEq.
+ := UsualEq <+ UsualIsEq.
 
 Module Type UsualDecidableType <: DecidableType
- := UsualEq <+ IsEq <+ HasEqDec.
+ := UsualEq <+ UsualIsEq <+ HasEqDec.
+
+Module Type UsualDecidableTypeOrig <: DecidableTypeOrig
+ := UsualEq <+ UsualIsEqOrig <+ HasEqDec.
 
 Module Type UsualDecidableTypeBoth <: DecidableTypeBoth
- := UsualEq <+ IsEq <+ IsEqOrig <+ HasEqDec.
+ := UsualEq <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqDec.
 
 Module Type UsualBoolEq := UsualEq <+ HasEqBool.
 
 Module Type UsualDecidableTypeFull <: DecidableTypeFull
- := UsualEq <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
+ := UsualEq <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqDec <+ HasEqBool.
 
 
 (** Some shortcuts for easily building a [UsualDecidableType] *)
 
 Module Type MiniDecidableType.
- Parameter t : Type.
+ Include Typ.
  Parameter eq_dec : forall x y : t, {x=y}+{~x=y}.
 End MiniDecidableType.
 
-Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth.
- Definition eq := @Logic.eq M.t.
- Include M <+ UsualIsEq <+ UsualIsEqOrig.
-End Make_UDT.
+Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth
+ := M <+ HasUsualEq <+ UsualIsEq <+ UsualIsEqOrig.
 
 Module Make_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull
  := M <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqBool2Dec.
diff --git a/theories/Structures/DecidableType2Facts.v b/theories/Structures/EqualitiesFacts.v
index 07a3b8f838..d9b1d76fdf 100644
--- a/theories/Structures/DecidableType2Facts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Import DecidableType2 Bool SetoidList RelationPairs.
+Require Import Equalities Bool SetoidList RelationPairs.
 
 (** In a BooleanEqualityType, [eqb] is compatible with [eq] *)
 
@@ -145,4 +145,41 @@ Module KeyDecidableType(Import D:DecidableType).
 End KeyDecidableType.
 
 
+(** * PairDecidableType 
+   
+   From two decidable types, we can build a new DecidableType
+   over their cartesian product. *)
 
+Module PairDecidableType(D1 D2:DecidableType) <: DecidableType.
+
+ Definition t := (D1.t * D2.t)%type.
+
+ Definition eq := (D1.eq * D2.eq)%signature.
+
+ Instance eq_equiv : Equivalence eq.
+
+ Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
+ Proof.
+ intros (x1,x2) (y1,y2); unfold eq; simpl.
+ destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
+  compute; intuition.
+ Defined.
+
+End PairDecidableType.
+
+(** Similarly for pairs of UsualDecidableType *)
+
+Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
+ Definition t := (D1.t * D2.t)%type.
+ Definition eq := @eq t.
+ Program Instance eq_equiv : Equivalence eq.
+ Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
+ Proof.
+ intros (x1,x2) (y1,y2);
+ destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
+ unfold eq, D1.eq, D2.eq in *; simpl;
+ (left; f_equal; auto; fail) ||
+ (right; intro H; injection H; auto).
+ Defined.
+
+End PairUsualDecidableType.
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index f45e43b445..232989fad0 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Import OrderTac OrderedType2 OrderedType2Facts Setoid Morphisms Basics.
+Require Import Orders OrdersTac OrdersFacts Setoid Morphisms Basics.
 
 (** * A Generic construction of min and max *)
 
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index 1f3e50dc3f..7d56d96665 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -8,10 +8,13 @@
 
 (* $Id$ *)
 
-Require Export SetoidList Morphisms OrderTac.
+Require Export SetoidList Morphisms OrdersTac.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+(** NB: This file is here only for compatibility with earlier version of
+     [FSets] and [FMap]. Please use [Structures/Orders.v] directly now. *)
+
 (** * Ordered types *)
 
 Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type :=
@@ -103,7 +106,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
   Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x.
   Proof. intros; destruct (compare x y); auto. Qed.
 
-  Module OrderElts <: OrderedType2.TotalOrder.
+  Module OrderElts <: Orders.TotalOrder.
   Definition t := t.
   Definition eq := eq.
   Definition lt := lt.
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/Orders.v
index 766b0faf05..c71be0a6ee 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/Orders.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Require Export Relations Morphisms Setoid DecidableType2.
+Require Export Relations Morphisms Setoid Equalities.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/theories/Structures/OrderedType2Alt.v b/theories/Structures/OrdersAlt.v
index b036b50e5b..261e75e1c5 100644
--- a/theories/Structures/OrderedType2Alt.v
+++ b/theories/Structures/OrdersAlt.v
@@ -13,7 +13,7 @@
 
 (* $Id$ *)
 
-Require Import OrderedType OrderedType2.
+Require Import OrderedType Orders.
 Set Implicit Arguments.
 
 (** * Some alternative (but equivalent) presentations for an Ordered Type
diff --git a/theories/Structures/OrderedType2Ex.v b/theories/Structures/OrdersEx.v
index 1e45a3fbfb..56f1d5dedd 100644
--- a/theories/Structures/OrderedType2Ex.v
+++ b/theories/Structures/OrdersEx.v
@@ -13,8 +13,8 @@
 
 (* $Id$ *)
 
-Require Import OrderedType2 NatOrderedType POrderedType NOrderedType
- ZOrderedType DecidableType2Ex RelationPairs.
+Require Import Orders NatOrderedType POrderedType NOrderedType
+ ZOrderedType RelationPairs EqualitiesFacts.
 
 (** * Examples of Ordered Type structures. *)
 
diff --git a/theories/Structures/OrderedType2Facts.v b/theories/Structures/OrdersFacts.v
index b5dc0c92fc..a318ecb858 100644
--- a/theories/Structures/OrderedType2Facts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -6,8 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Import Basics OrderTac.
-Require Export OrderedType2.
+Require Import Basics OrdersTac.
+Require Export Orders.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Structures/OrderedType2Lists.v b/theories/Structures/OrdersLists.v
index 79690fb024..2ed0702688 100644
--- a/theories/Structures/OrderedType2Lists.v
+++ b/theories/Structures/OrdersLists.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Export RelationPairs SetoidList OrderedType2.
+Require Export RelationPairs SetoidList Orders.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrdersTac.v
index 2465dc539e..80be890265 100644
--- a/theories/Structures/OrderTac.v
+++ b/theories/Structures/OrdersTac.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Import Setoid Morphisms Basics DecidableType2 OrderedType2.
+Require Import Setoid Morphisms Basics Equalities Orders.
 Set Implicit Arguments.
 
 (** * The order tactic *)
diff --git a/theories/Structures/vo.itarget b/theories/Structures/vo.itarget
index 6500dcd89a..674e9fba9d 100644
--- a/theories/Structures/vo.itarget
+++ b/theories/Structures/vo.itarget
@@ -1,15 +1,14 @@
+Equalities.vo
+EqualitiesFacts.vo
+Orders.vo
+OrdersEx.vo
+OrdersFacts.vo
+OrdersLists.vo
+OrdersTac.vo
+OrdersAlt.vo
+GenericMinMax.vo
+DecidableType.vo
+DecidableTypeEx.vo
 OrderedTypeAlt.vo
 OrderedTypeEx.vo
 OrderedType.vo
-DecidableType.vo
-DecidableTypeEx.vo
-OrderedType2Alt.vo
-OrderedType2Ex.vo
-OrderedType2.vo
-OrderedType2Facts.vo
-OrderedType2Lists.vo
-DecidableType2.vo
-DecidableType2Ex.vo
-DecidableType2Facts.vo
-OrderTac.vo
-GenericMinMax.vo
diff --git a/theories/ZArith/ZOrderedType.v b/theories/ZArith/ZOrderedType.v
index f249ae1b42..570e2a4d6f 100644
--- a/theories/ZArith/ZOrderedType.v
+++ b/theories/ZArith/ZOrderedType.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 Require Import BinInt Zcompare Zorder Zbool ZArith_dec
- DecidableType2 OrderedType2 OrderTac.
+ Equalities Orders OrdersTac.
 
 Local Open Scope Z_scope.
 
diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v
index 108e74bea3..c1657e2984 100644
--- a/theories/ZArith/Zminmax.v
+++ b/theories/ZArith/Zminmax.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import OrderedType2 BinInt Zcompare Zorder ZOrderedType
+Require Import Orders BinInt Zcompare Zorder ZOrderedType
  GenericMinMax.
 
 (** * Maximum and Minimum of two [Z] numbers *)