From 5794a55f9e8b39b8e562e70593ab794abf463a86 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 7 Jan 2010 15:32:52 +0000
Subject: 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
---
 theories/Arith/MinMax.v                   |   2 +-
 theories/Arith/NatOrderedType.v           |   2 +-
 theories/FSets/FSetAVL.v                  |   4 +-
 theories/FSets/FSetCompat.v               |   4 +-
 theories/FSets/FSetList.v                 |   4 +-
 theories/FSets/FSetWeakList.v             |   4 +-
 theories/MSets/MSetInterface.v            |   2 +-
 theories/MSets/MSetList.v                 |   2 +-
 theories/MSets/MSetProperties.v           |   2 +-
 theories/MSets/MSetToFiniteSet.v          |   2 +-
 theories/MSets/MSets.v                    |   9 +-
 theories/NArith/NOrderedType.v            |   2 +-
 theories/NArith/Nminmax.v                 |   2 +-
 theories/NArith/POrderedType.v            |   2 +-
 theories/NArith/Pminmax.v                 |   2 +-
 theories/Numbers/NatInt/NZAxioms.v        |   2 +-
 theories/Numbers/NatInt/NZOrder.v         |   2 +-
 theories/QArith/QOrderedType.v            |   2 +-
 theories/QArith/Qminmax.v                 |   2 +-
 theories/Reals/ROrderedType.v             |   2 +-
 theories/Reals/Rminmax.v                  |   2 +-
 theories/Structures/DecidableType.v       |   8 +-
 theories/Structures/DecidableType2.v      | 214 --------------------
 theories/Structures/DecidableType2Ex.v    |  53 -----
 theories/Structures/DecidableType2Facts.v | 148 --------------
 theories/Structures/DecidableTypeEx.v     |  27 +--
 theories/Structures/Equalities.v          | 216 ++++++++++++++++++++
 theories/Structures/EqualitiesFacts.v     | 185 +++++++++++++++++
 theories/Structures/GenericMinMax.v       |   2 +-
 theories/Structures/OrderTac.v            | 323 ------------------------------
 theories/Structures/OrderedType.v         |   7 +-
 theories/Structures/OrderedType2.v        | 160 ---------------
 theories/Structures/OrderedType2Alt.v     | 243 ----------------------
 theories/Structures/OrderedType2Ex.v      |  88 --------
 theories/Structures/OrderedType2Facts.v   | 234 ----------------------
 theories/Structures/OrderedType2Lists.v   | 256 -----------------------
 theories/Structures/Orders.v              | 160 +++++++++++++++
 theories/Structures/OrdersAlt.v           | 243 ++++++++++++++++++++++
 theories/Structures/OrdersEx.v            |  88 ++++++++
 theories/Structures/OrdersFacts.v         | 234 ++++++++++++++++++++++
 theories/Structures/OrdersLists.v         | 256 +++++++++++++++++++++++
 theories/Structures/OrdersTac.v           | 323 ++++++++++++++++++++++++++++++
 theories/Structures/vo.itarget            |  23 +--
 theories/ZArith/ZOrderedType.v            |   2 +-
 theories/ZArith/Zminmax.v                 |   2 +-
 45 files changed, 1764 insertions(+), 1788 deletions(-)
 delete mode 100644 theories/Structures/DecidableType2.v
 delete mode 100644 theories/Structures/DecidableType2Ex.v
 delete mode 100644 theories/Structures/DecidableType2Facts.v
 create mode 100644 theories/Structures/Equalities.v
 create mode 100644 theories/Structures/EqualitiesFacts.v
 delete mode 100644 theories/Structures/OrderTac.v
 delete mode 100644 theories/Structures/OrderedType2.v
 delete mode 100644 theories/Structures/OrderedType2Alt.v
 delete mode 100644 theories/Structures/OrderedType2Ex.v
 delete mode 100644 theories/Structures/OrderedType2Facts.v
 delete mode 100644 theories/Structures/OrderedType2Lists.v
 create mode 100644 theories/Structures/Orders.v
 create mode 100644 theories/Structures/OrdersAlt.v
 create mode 100644 theories/Structures/OrdersEx.v
 create mode 100644 theories/Structures/OrdersFacts.v
 create mode 100644 theories/Structures/OrdersLists.v
 create mode 100644 theories/Structures/OrdersTac.v

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/DecidableType2.v b/theories/Structures/DecidableType2.v
deleted file mode 100644
index 2679d25b01..0000000000
--- a/theories/Structures/DecidableType2.v
+++ /dev/null
@@ -1,214 +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 Export RelationClasses.
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-(** * Structure with just a base type [t] *)
-
-Module Type Typ.
-  Parameter Inline t : Type.
-End Typ.
-
-(** * Structure with an equality relation [eq] *)
-
-Module Type HasEq (Import T:Typ).
-  Parameter Inline eq : t -> t -> Prop.
-End HasEq.
-
-Module Type Eq := Typ <+ HasEq.
-
-Module Type EqNotation (Import E:Eq).
-  Infix "==" := eq (at level 70, no associativity).
-  Notation "x ~= y" := (~eq x y) (at level 70, no associativity).
-End EqNotation.
-
-Module Type Eq' := Eq <+ EqNotation.
-
-(** * Specification of the equality via the [Equivalence] type class *)
-
-Module Type IsEq (Import E:Eq).
-  Declare Instance eq_equiv : Equivalence eq.
-End IsEq.
-
-(** * Earlier specification of equality by three separate lemmas. *)
-
-Module Type IsEqOrig (Import E:Eq').
-  Axiom eq_refl : forall x : t, x==x.
-  Axiom eq_sym : forall x y : t, x==y -> y==x.
-  Axiom eq_trans : forall x y z : t, x==y -> y==z -> x==z.
-  Hint Immediate eq_sym.
-  Hint Resolve eq_refl eq_trans.
-End IsEqOrig.
-
-(** * Types with decidable equality *)
-
-Module Type HasEqDec (Import E:Eq').
-  Parameter eq_dec : forall x y : t, { x==y } + { ~ x==y }.
-End HasEqDec.
-
-(** * Boolean Equality *)
-
-(** Having [eq_dec] is the same as having a boolean equality plus
-    a correctness proof. *)
-
-Module Type HasEqBool (Import E:Eq').
-  Parameter Inline eqb : t -> t -> bool.
-  Parameter eqb_eq : forall x y, eqb x y = true <-> x==y.
-End HasEqBool.
-
-(** From these basic blocks, we can build many combinations
-    of static standalone module types. *)
-
-Module Type EqualityType := Eq <+ IsEq.
-
-Module Type EqualityTypeOrig := Eq <+ IsEqOrig.
-
-Module Type EqualityTypeBoth <: EqualityType <: EqualityTypeOrig
- := Eq <+ IsEq <+ IsEqOrig.
-
-Module Type DecidableType <: EqualityType
- := Eq <+ IsEq <+ HasEqDec.
-
-Module Type DecidableTypeOrig <: EqualityTypeOrig
- := Eq <+ IsEqOrig <+ HasEqDec.
-
-Module Type DecidableTypeBoth <: DecidableType <: DecidableTypeOrig
- := EqualityTypeBoth <+ HasEqDec.
-
-Module Type BooleanEqualityType <: EqualityType
- := Eq <+ IsEq <+ HasEqBool.
-
-Module Type BooleanDecidableType <: DecidableType <: BooleanEqualityType
- := Eq <+ IsEq <+ HasEqDec <+ HasEqBool.
-
-Module Type DecidableTypeFull <: DecidableTypeBoth <: BooleanDecidableType
- := Eq <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
-
-(** Same, with notation for [eq] *)
-
-Module Type EqualityType' := EqualityType <+ EqNotation.
-Module Type EqualityTypeOrig' := EqualityTypeOrig <+ EqNotation.
-Module Type EqualityTypeBoth' := EqualityTypeBoth <+ EqNotation.
-Module Type DecidableType' := DecidableType <+ EqNotation.
-Module Type DecidableTypeOrig' := DecidableTypeOrig <+ EqNotation.
-Module Type DecidableTypeBoth' := DecidableTypeBoth <+ EqNotation.
-Module Type BooleanEqualityType' := BooleanEqualityType <+ EqNotation.
-Module Type BooleanDecidableType' := BooleanDecidableType <+ EqNotation.
-Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation.
-
-(** * Compatibility wrapper from/to the old version of
-      [EqualityType] and [DecidableType] *)
-
-Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E.
- Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
- Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
- Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
-End BackportEq.
-
-Module UpdateEq (E:Eq)(F:IsEqOrig E) <: IsEq E.
- Instance eq_equiv : Equivalence E.eq.
- Proof. exact (Build_Equivalence _ _ F.eq_refl F.eq_sym F.eq_trans). Qed.
-End UpdateEq.
-
-Module Backport_ET (E:EqualityType) <: EqualityTypeBoth
- := E <+ BackportEq.
-
-Module Update_ET (E:EqualityTypeOrig) <: EqualityTypeBoth
- := E <+ UpdateEq.
-
-Module Backport_DT (E:DecidableType) <: DecidableTypeBoth
- := E <+ BackportEq.
-
-Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth
- := E <+ UpdateEq.
-
-
-(** * Having [eq_dec] is equivalent to having [eqb] and its spec. *)
-
-Module HasEqDec2Bool (E:Eq)(F:HasEqDec E) <: HasEqBool E.
- Definition eqb x y := if F.eq_dec x y then true else false.
- Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y.
- Proof.
-  intros x y. unfold eqb. destruct F.eq_dec as [EQ|NEQ].
-  auto with *.
-  split. discriminate. intro EQ; elim NEQ; auto.
- Qed.
-End HasEqDec2Bool.
-
-Module HasEqBool2Dec (E:Eq)(F:HasEqBool E) <: HasEqDec E.
- Lemma eq_dec : forall x y, {E.eq x y}+{~E.eq x y}.
- Proof.
-  intros x y. assert (H:=F.eqb_eq x y).
-  destruct (F.eqb x y); [left|right].
-  apply -> H; auto.
-  intro EQ. apply H in EQ. discriminate.
- Defined.
-End HasEqBool2Dec.
-
-Module Dec2Bool (E:DecidableType) <: BooleanDecidableType
- := E <+ HasEqDec2Bool.
-
-Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType
- := E <+ HasEqBool2Dec.
-
-
-
-(** * UsualDecidableType
-
-   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 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.
-End UsualIsEqOrig.
-
-Module Type UsualEqualityType <: EqualityType
- := UsualEq <+ IsEq.
-
-Module Type UsualDecidableType <: DecidableType
- := UsualEq <+ IsEq <+ HasEqDec.
-
-Module Type UsualDecidableTypeBoth <: DecidableTypeBoth
- := UsualEq <+ IsEq <+ IsEqOrig <+ HasEqDec.
-
-Module Type UsualBoolEq := UsualEq <+ HasEqBool.
-
-Module Type UsualDecidableTypeFull <: DecidableTypeFull
- := UsualEq <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
-
-
-(** Some shortcuts for easily building a [UsualDecidableType] *)
-
-Module Type MiniDecidableType.
- Parameter t : Type.
- 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_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull
- := M <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqBool2Dec.
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/DecidableType2Facts.v b/theories/Structures/DecidableType2Facts.v
deleted file mode 100644
index 07a3b8f838..0000000000
--- a/theories/Structures/DecidableType2Facts.v
+++ /dev/null
@@ -1,148 +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       *)
-(***********************************************************************)
-
-Require Import DecidableType2 Bool SetoidList RelationPairs.
-
-(** In a BooleanEqualityType, [eqb] is compatible with [eq] *)
-
-Module BoolEqualityFacts (Import E : BooleanEqualityType).
-
-Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb.
-Proof.
-intros x x' Exx' y y' Eyy'.
-apply eq_true_iff_eq.
-rewrite 2 eqb_eq, Exx', Eyy'; auto with *.
-Qed.
-
-End BoolEqualityFacts.
-
-
-(** * Keys and datas used in FMap *)
-Module KeyDecidableType(Import D:DecidableType).
-
- Section Elt.
- Variable elt : Type.
- Notation key:=t.
-
-  Local Open Scope signature_scope.
-
-  Definition eqk : relation (key*elt) := eq @@1.
-  Definition eqke : relation (key*elt) := eq * Logic.eq.
-  Hint Unfold eqk eqke.
-
-  (* eqke is stricter than eqk *)
-
-  Global Instance eqke_eqk : subrelation eqke eqk.
-  Proof. firstorder. Qed.
-
-  (* eqk, eqke are equalities, ltk is a strict order *)
-
-  Global Instance eqk_equiv : Equivalence eqk.
-
-  Global Instance eqke_equiv : Equivalence eqke.
-
-  (* Additionnal facts *)
-
-  Lemma InA_eqke_eqk :
-     forall x m, InA eqke x m -> InA eqk x m.
-  Proof.
-    unfold eqke, RelProd; induction 1; firstorder.
-  Qed.
-  Hint Resolve InA_eqke_eqk.
-
-  Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
-  Proof.
-   intros. rewrite <- H; auto.
-  Qed.
-
-  Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
-  Definition In k m := exists e:elt, MapsTo k e m.
-
-  Hint Unfold MapsTo In.
-
-  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
-
-  Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
-  Proof.
-  firstorder.
-  exists x; auto.
-  induction H.
-  destruct y; compute in H.
-  exists e; left; auto.
-  destruct IHInA as [e H0].
-  exists e; auto.
-  Qed.
-
-  Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l.
-  Proof.
-  unfold In, MapsTo.
-  setoid_rewrite Exists_exists; setoid_rewrite InA_alt.
-  firstorder.
-  exists (snd x), x; auto.
-  Qed.
-
-  Lemma In_nil : forall k, In k nil <-> False.
-  Proof.
-  intros; rewrite In_alt2; apply Exists_nil.
-  Qed.
-
-  Lemma In_cons : forall k p l,
-   In k (p::l) <-> eq k (fst p) \/ In k l.
-  Proof.
-  intros; rewrite !In_alt2, Exists_cons; intuition.
-  Qed.
-
-  Global Instance MapsTo_compat :
-   Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo.
-  Proof.
-  intros x x' Hx e e' He l l' Hl. unfold MapsTo.
-  rewrite Hx, He, Hl; intuition.
-  Qed.
-
-  Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In.
-  Proof.
-  intros x x' Hx l l' Hl. rewrite !In_alt.
-  setoid_rewrite Hl. setoid_rewrite Hx. intuition.
-  Qed.
-
-  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
-  Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed.
-
-  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
-  Proof. intros l x y EQ. rewrite <- EQ; auto. Qed.
-
-  Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
-  Proof.
-    intros; invlist In; invlist MapsTo. compute in * |- ; intuition.
-    right; exists x; auto.
-  Qed.
-
-  Lemma In_inv_2 : forall k k' e e' l,
-      InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
-  Proof.
-   intros; invlist InA; intuition.
-  Qed.
-
-  Lemma In_inv_3 : forall x x' l,
-      InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
-  Proof.
-   intros; invlist InA; compute in * |- ; intuition.
-  Qed.
-
- End Elt.
-
- Hint Unfold eqk eqke.
- Hint Extern 2 (eqke ?a ?b) => split.
- Hint Resolve InA_eqke_eqk.
- Hint Unfold MapsTo In.
- Hint Resolve In_inv_2 In_inv_3.
-
-End KeyDecidableType.
-
-
-
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/Equalities.v b/theories/Structures/Equalities.v
new file mode 100644
index 0000000000..76f539764a
--- /dev/null
+++ b/theories/Structures/Equalities.v
@@ -0,0 +1,216 @@
+(***********************************************************************)
+(*  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 Export RelationClasses.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Structure with just a base type [t] *)
+
+Module Type Typ.
+  Parameter Inline t : Type.
+End Typ.
+
+(** * Structure with an equality relation [eq] *)
+
+Module Type HasEq (Import T:Typ).
+  Parameter Inline eq : t -> t -> Prop.
+End HasEq.
+
+Module Type Eq := Typ <+ HasEq.
+
+Module Type EqNotation (Import E:Eq).
+  Infix "==" := eq (at level 70, no associativity).
+  Notation "x ~= y" := (~eq x y) (at level 70, no associativity).
+End EqNotation.
+
+Module Type Eq' := Eq <+ EqNotation.
+
+(** * Specification of the equality via the [Equivalence] type class *)
+
+Module Type IsEq (Import E:Eq).
+  Declare Instance eq_equiv : Equivalence eq.
+End IsEq.
+
+(** * Earlier specification of equality by three separate lemmas. *)
+
+Module Type IsEqOrig (Import E:Eq').
+  Axiom eq_refl : forall x : t, x==x.
+  Axiom eq_sym : forall x y : t, x==y -> y==x.
+  Axiom eq_trans : forall x y z : t, x==y -> y==z -> x==z.
+  Hint Immediate eq_sym.
+  Hint Resolve eq_refl eq_trans.
+End IsEqOrig.
+
+(** * Types with decidable equality *)
+
+Module Type HasEqDec (Import E:Eq').
+  Parameter eq_dec : forall x y : t, { x==y } + { ~ x==y }.
+End HasEqDec.
+
+(** * Boolean Equality *)
+
+(** Having [eq_dec] is the same as having a boolean equality plus
+    a correctness proof. *)
+
+Module Type HasEqBool (Import E:Eq').
+  Parameter Inline eqb : t -> t -> bool.
+  Parameter eqb_eq : forall x y, eqb x y = true <-> x==y.
+End HasEqBool.
+
+(** From these basic blocks, we can build many combinations
+    of static standalone module types. *)
+
+Module Type EqualityType := Eq <+ IsEq.
+
+Module Type EqualityTypeOrig := Eq <+ IsEqOrig.
+
+Module Type EqualityTypeBoth <: EqualityType <: EqualityTypeOrig
+ := Eq <+ IsEq <+ IsEqOrig.
+
+Module Type DecidableType <: EqualityType
+ := Eq <+ IsEq <+ HasEqDec.
+
+Module Type DecidableTypeOrig <: EqualityTypeOrig
+ := Eq <+ IsEqOrig <+ HasEqDec.
+
+Module Type DecidableTypeBoth <: DecidableType <: DecidableTypeOrig
+ := EqualityTypeBoth <+ HasEqDec.
+
+Module Type BooleanEqualityType <: EqualityType
+ := Eq <+ IsEq <+ HasEqBool.
+
+Module Type BooleanDecidableType <: DecidableType <: BooleanEqualityType
+ := Eq <+ IsEq <+ HasEqDec <+ HasEqBool.
+
+Module Type DecidableTypeFull <: DecidableTypeBoth <: BooleanDecidableType
+ := Eq <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
+
+(** Same, with notation for [eq] *)
+
+Module Type EqualityType' := EqualityType <+ EqNotation.
+Module Type EqualityTypeOrig' := EqualityTypeOrig <+ EqNotation.
+Module Type EqualityTypeBoth' := EqualityTypeBoth <+ EqNotation.
+Module Type DecidableType' := DecidableType <+ EqNotation.
+Module Type DecidableTypeOrig' := DecidableTypeOrig <+ EqNotation.
+Module Type DecidableTypeBoth' := DecidableTypeBoth <+ EqNotation.
+Module Type BooleanEqualityType' := BooleanEqualityType <+ EqNotation.
+Module Type BooleanDecidableType' := BooleanDecidableType <+ EqNotation.
+Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation.
+
+(** * Compatibility wrapper from/to the old version of
+      [EqualityType] and [DecidableType] *)
+
+Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E.
+ Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
+ Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
+ Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
+End BackportEq.
+
+Module UpdateEq (E:Eq)(F:IsEqOrig E) <: IsEq E.
+ Instance eq_equiv : Equivalence E.eq.
+ Proof. exact (Build_Equivalence _ _ F.eq_refl F.eq_sym F.eq_trans). Qed.
+End UpdateEq.
+
+Module Backport_ET (E:EqualityType) <: EqualityTypeBoth
+ := E <+ BackportEq.
+
+Module Update_ET (E:EqualityTypeOrig) <: EqualityTypeBoth
+ := E <+ UpdateEq.
+
+Module Backport_DT (E:DecidableType) <: DecidableTypeBoth
+ := E <+ BackportEq.
+
+Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth
+ := E <+ UpdateEq.
+
+
+(** * Having [eq_dec] is equivalent to having [eqb] and its spec. *)
+
+Module HasEqDec2Bool (E:Eq)(F:HasEqDec E) <: HasEqBool E.
+ Definition eqb x y := if F.eq_dec x y then true else false.
+ Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y.
+ Proof.
+  intros x y. unfold eqb. destruct F.eq_dec as [EQ|NEQ].
+  auto with *.
+  split. discriminate. intro EQ; elim NEQ; auto.
+ Qed.
+End HasEqDec2Bool.
+
+Module HasEqBool2Dec (E:Eq)(F:HasEqBool E) <: HasEqDec E.
+ Lemma eq_dec : forall x y, {E.eq x y}+{~E.eq x y}.
+ Proof.
+  intros x y. assert (H:=F.eqb_eq x y).
+  destruct (F.eqb x y); [left|right].
+  apply -> H; auto.
+  intro EQ. apply H in EQ. discriminate.
+ Defined.
+End HasEqBool2Dec.
+
+Module Dec2Bool (E:DecidableType) <: BooleanDecidableType
+ := E <+ HasEqDec2Bool.
+
+Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType
+ := E <+ HasEqBool2Dec.
+
+
+
+(** * UsualDecidableType
+
+   A particular case of [DecidableType] where the equality is
+   the usual one of Coq. *)
+
+Module Type HasUsualEq (Import T:Typ) <: HasEq T.
+ Definition eq := @Logic.eq t.
+End HasUsualEq.
+
+Module Type UsualEq <: Eq := Typ <+ HasUsualEq.
+
+Module Type UsualIsEq (E:UsualEq) <: IsEq E.
+ Program Instance eq_equiv : Equivalence E.eq.
+End UsualIsEq.
+
+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 <+ UsualIsEq.
+
+Module Type UsualDecidableType <: DecidableType
+ := UsualEq <+ UsualIsEq <+ HasEqDec.
+
+Module Type UsualDecidableTypeOrig <: DecidableTypeOrig
+ := UsualEq <+ UsualIsEqOrig <+ HasEqDec.
+
+Module Type UsualDecidableTypeBoth <: DecidableTypeBoth
+ := UsualEq <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqDec.
+
+Module Type UsualBoolEq := UsualEq <+ HasEqBool.
+
+Module Type UsualDecidableTypeFull <: DecidableTypeFull
+ := UsualEq <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqDec <+ HasEqBool.
+
+
+(** Some shortcuts for easily building a [UsualDecidableType] *)
+
+Module Type MiniDecidableType.
+ Include Typ.
+ Parameter eq_dec : forall x y : t, {x=y}+{~x=y}.
+End MiniDecidableType.
+
+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/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
new file mode 100644
index 0000000000..d9b1d76fdf
--- /dev/null
+++ b/theories/Structures/EqualitiesFacts.v
@@ -0,0 +1,185 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+Require Import Equalities Bool SetoidList RelationPairs.
+
+(** In a BooleanEqualityType, [eqb] is compatible with [eq] *)
+
+Module BoolEqualityFacts (Import E : BooleanEqualityType).
+
+Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb.
+Proof.
+intros x x' Exx' y y' Eyy'.
+apply eq_true_iff_eq.
+rewrite 2 eqb_eq, Exx', Eyy'; auto with *.
+Qed.
+
+End BoolEqualityFacts.
+
+
+(** * Keys and datas used in FMap *)
+Module KeyDecidableType(Import D:DecidableType).
+
+ Section Elt.
+ Variable elt : Type.
+ Notation key:=t.
+
+  Local Open Scope signature_scope.
+
+  Definition eqk : relation (key*elt) := eq @@1.
+  Definition eqke : relation (key*elt) := eq * Logic.eq.
+  Hint Unfold eqk eqke.
+
+  (* eqke is stricter than eqk *)
+
+  Global Instance eqke_eqk : subrelation eqke eqk.
+  Proof. firstorder. Qed.
+
+  (* eqk, eqke are equalities, ltk is a strict order *)
+
+  Global Instance eqk_equiv : Equivalence eqk.
+
+  Global Instance eqke_equiv : Equivalence eqke.
+
+  (* Additionnal facts *)
+
+  Lemma InA_eqke_eqk :
+     forall x m, InA eqke x m -> InA eqk x m.
+  Proof.
+    unfold eqke, RelProd; induction 1; firstorder.
+  Qed.
+  Hint Resolve InA_eqke_eqk.
+
+  Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
+  Proof.
+   intros. rewrite <- H; auto.
+  Qed.
+
+  Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
+  Definition In k m := exists e:elt, MapsTo k e m.
+
+  Hint Unfold MapsTo In.
+
+  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
+
+  Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
+  Proof.
+  firstorder.
+  exists x; auto.
+  induction H.
+  destruct y; compute in H.
+  exists e; left; auto.
+  destruct IHInA as [e H0].
+  exists e; auto.
+  Qed.
+
+  Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l.
+  Proof.
+  unfold In, MapsTo.
+  setoid_rewrite Exists_exists; setoid_rewrite InA_alt.
+  firstorder.
+  exists (snd x), x; auto.
+  Qed.
+
+  Lemma In_nil : forall k, In k nil <-> False.
+  Proof.
+  intros; rewrite In_alt2; apply Exists_nil.
+  Qed.
+
+  Lemma In_cons : forall k p l,
+   In k (p::l) <-> eq k (fst p) \/ In k l.
+  Proof.
+  intros; rewrite !In_alt2, Exists_cons; intuition.
+  Qed.
+
+  Global Instance MapsTo_compat :
+   Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo.
+  Proof.
+  intros x x' Hx e e' He l l' Hl. unfold MapsTo.
+  rewrite Hx, He, Hl; intuition.
+  Qed.
+
+  Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In.
+  Proof.
+  intros x x' Hx l l' Hl. rewrite !In_alt.
+  setoid_rewrite Hl. setoid_rewrite Hx. intuition.
+  Qed.
+
+  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
+  Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed.
+
+  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
+  Proof. intros l x y EQ. rewrite <- EQ; auto. Qed.
+
+  Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
+  Proof.
+    intros; invlist In; invlist MapsTo. compute in * |- ; intuition.
+    right; exists x; auto.
+  Qed.
+
+  Lemma In_inv_2 : forall k k' e e' l,
+      InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
+  Proof.
+   intros; invlist InA; intuition.
+  Qed.
+
+  Lemma In_inv_3 : forall x x' l,
+      InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
+  Proof.
+   intros; invlist InA; compute in * |- ; intuition.
+  Qed.
+
+ End Elt.
+
+ Hint Unfold eqk eqke.
+ Hint Extern 2 (eqke ?a ?b) => split.
+ Hint Resolve InA_eqke_eqk.
+ Hint Unfold MapsTo In.
+ Hint Resolve In_inv_2 In_inv_3.
+
+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/OrderTac.v b/theories/Structures/OrderTac.v
deleted file mode 100644
index 2465dc539e..0000000000
--- a/theories/Structures/OrderTac.v
+++ /dev/null
@@ -1,323 +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       *)
-(***********************************************************************)
-
-Require Import Setoid Morphisms Basics DecidableType2 OrderedType2.
-Set Implicit Arguments.
-
-(** * The order tactic *)
-
-(** This tactic is designed to solve systems of (in)equations
-    involving [eq], [lt], [le] and [~eq] on some type. This tactic is
-    domain-agnostic; it will only use equivalence+order axioms, and
-    not analyze elements of the domain. Hypothesis or goal of the form
-    [~lt] or [~le] are initially turned into [le] and [lt], other
-    parts of the goal are ignored. This initial preparation of the
-    goal is the only moment where totality is used. In particular,
-    the core of the tactic only proceeds by saturation of transitivity
-    and similar properties, and does not perform case splitting.
-    The tactic will fail if it doesn't solve the goal. *)
-
-
-(** An abstract vision of the predicates. This allows a one-line
-    statement for interesting transitivity properties: for instance
-    [trans_ord OLE OLE = OLE] will imply later
-    [le x y -> le y z -> le x z].
-*)
-
-Inductive ord := OEQ | OLT | OLE.
-Definition trans_ord o o' :=
- match o, o' with
- | OEQ, _ => o'
- | _, OEQ => o
- | OLE, OLE => OLE
- | _, _ => OLT
- end.
-Local Infix "+" := trans_ord.
-
-
-(** ** The requirements of the tactic : [TotalOrder].
-
-   [TotalOrder] contains an equivalence [eq],
-   a strict order [lt] total and compatible with [eq], and
-   a larger order [le] synonym for [lt\/eq].
-
-  NB: we create here a clone of TotalOrder, but without the [Inline] Pragma.
-  This is important for having later the exact shape in Ltac matching.
-*)
-
-Module Type TotalOrder_NoInline <: TotalOrder.
- Parameter Inline t : Type.
- Parameters eq lt le : t -> t -> Prop.
- Include IsEq <+ IsStrOrder <+ LeIsLtEq <+ LtIsTotal.
-End TotalOrder_NoInline.
-
-Module Type TotalOrder_NoInline' := TotalOrder_NoInline <+ EqLtLeNotation.
-
-(** We make explicit aliases to help ltac matching *)
-
-Module CloneOrder (O:TotalOrder_NoInline) <: TotalOrder.
-Definition t := O.t.
-Definition eq := O.eq.
-Definition lt := O.lt.
-Definition le := O.le.
-Definition eq_equiv := O.eq_equiv.
-Definition lt_compat := O.lt_compat.
-Definition lt_strorder := O.lt_strorder.
-Definition le_lteq := O.le_lteq.
-Definition lt_total := O.lt_total.
-End CloneOrder.
-
-
-
-(** ** Properties that will be used by the [order] tactic *)
-
-Module OrderFacts(Import O:TotalOrder_NoInline').
-
-(** Reflexivity rules *)
-
-Lemma eq_refl : forall x, x==x.
-Proof. reflexivity. Qed.
-
-Lemma le_refl : forall x, x<=x.
-Proof. intros; rewrite le_lteq; right; reflexivity. Qed.
-
-Lemma lt_irrefl : forall x, ~ x<x.
-Proof. intros; apply StrictOrder_Irreflexive. Qed.
-
-(** Symmetry rules *)
-
-Lemma eq_sym : forall x y, x==y -> y==x.
-Proof. auto with *. Qed.
-
-Lemma le_antisym : forall x y, x<=y -> y<=x -> x==y.
-Proof.
- intros x y; rewrite 2 le_lteq. intuition.
- elim (StrictOrder_Irreflexive x); transitivity y; auto.
-Qed.
-
-Lemma neq_sym : forall x y, ~x==y -> ~y==x.
-Proof. auto using eq_sym. Qed.
-
-(** Transitivity rules : first, a generic formulation, then instances*)
-
-Ltac subst_eqns :=
- match goal with
-   | H : _==_ |- _ => (rewrite H || rewrite <- H); clear H; subst_eqns
-   | _ => idtac
- end.
-
-Definition interp_ord o :=
- match o with OEQ => O.eq | OLT => O.lt | OLE => O.le end.
-Local Notation "#" := interp_ord.
-
-Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z.
-Proof.
-destruct o, o'; simpl; intros x y z; rewrite ?le_lteq; intuition;
- subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
-Qed.
-
-Definition eq_trans x y z : x==y -> y==z -> x==z := @trans OEQ OEQ x y z.
-Definition le_trans x y z : x<=y -> y<=z -> x<=z := @trans OLE OLE x y z.
-Definition lt_trans x y z : x<y -> y<z -> x<z := @trans OLT OLT x y z.
-Definition le_lt_trans x y z : x<=y -> y<z -> x<z := @trans OLE OLT x y z.
-Definition lt_le_trans x y z : x<y -> y<=z -> x<z := @trans OLT OLE x y z.
-Definition eq_lt x y z : x==y -> y<z -> x<z := @trans OEQ OLT x y z.
-Definition lt_eq x y z : x<y -> y==z -> x<z := @trans OLT OEQ x y z.
-Definition eq_le x y z : x==y -> y<=z -> x<=z := @trans OEQ OLE x y z.
-Definition le_eq x y z : x<=y -> y==z -> x<=z := @trans OLE OEQ x y z.
-
-Lemma eq_neq : forall x y z, x==y -> ~y==z -> ~x==z.
-Proof. eauto using eq_trans, eq_sym. Qed.
-
-Lemma neq_eq : forall x y z, ~x==y -> y==z -> ~x==z.
-Proof. eauto using eq_trans, eq_sym. Qed.
-
-(** (double) negation rules *)
-
-Lemma not_neq_eq : forall x y, ~~x==y -> x==y.
-Proof.
-intros x y H. destruct (lt_total x y) as [H'|[H'|H']]; auto;
- destruct H; intro H; rewrite H in H'; eapply lt_irrefl; eauto.
-Qed.
-
-Lemma not_ge_lt : forall x y, ~y<=x -> x<y.
-Proof.
-intros x y H. destruct (lt_total x y); auto.
-destruct H. rewrite le_lteq. intuition.
-Qed.
-
-Lemma not_gt_le : forall x y, ~y<x -> x<=y.
-Proof.
-intros x y H. rewrite le_lteq. generalize (lt_total x y); intuition.
-Qed.
-
-Lemma le_neq_lt : forall x y, x<=y -> ~x==y -> x<y.
-Proof. auto using not_ge_lt, le_antisym. Qed.
-
-End OrderFacts.
-
-
-
-(** ** [MakeOrderTac] : The functor providing the order tactic. *)
-
-Module MakeOrderTac (Import O:TotalOrder_NoInline').
-
-Include OrderFacts O.
-
-(** order_eq : replace x by y in all (in)equations hyps thanks
-   to equality EQ (where eq has been hidden in order to avoid
-   self-rewriting), then discard EQ. *)
-
-Ltac order_rewr x eqn :=
- (* NB: we could use the real rewrite here, but proofs would be uglier. *)
- let rewr H t := generalize t; clear H; intro H
- in
- match goal with
- | H : x == _ |- _ => rewr H (eq_trans (eq_sym eqn) H); order_rewr x eqn
- | H : _ == x |- _ => rewr H (eq_trans H eqn); order_rewr x eqn
- | H : ~x == _ |- _ => rewr H (eq_neq (eq_sym eqn) H); order_rewr x eqn
- | H : ~_ == x |- _ => rewr H (neq_eq H eqn); order_rewr x eqn
- | H : x < _ |- _ => rewr H (eq_lt (eq_sym eqn) H); order_rewr x eqn
- | H : _ < x |- _ => rewr H (lt_eq H eqn); order_rewr x eqn
- | H : x <= _ |- _ => rewr H (eq_le (eq_sym eqn) H); order_rewr x eqn
- | H : _ <= x |- _ => rewr H (le_eq H eqn); order_rewr x eqn
- | _ => clear eqn
-end.
-
-Ltac order_eq x y eqn :=
- match x with
- | y => clear eqn
- | _ => change (interp_ord OEQ x y) in eqn; order_rewr x eqn
- end.
-
-(** Goal preparation : We turn all negative hyps into positive ones
-  and try to prove False from the inverse of the current goal.
-  These steps require totality of our order. After this preparation,
-  order only deals with the context, and tries to prove False.
-  Hypotheses of the form [A -> False] are also folded in [~A]
-  for convenience (i.e. cope with the mess left by intuition). *)
-
-Ltac order_prepare :=
- match goal with
- | H : ?A -> False |- _ => change (~A) in H; order_prepare
- | H : ~(?R ?x ?y) |- _ =>
-   match R with
-   | eq => fail 1 (* if already using [eq], we leave it this ways *)
-   | _ => (change (~x==y) in H ||
-           apply not_gt_le in H ||
-           apply not_ge_lt in H ||
-           clear H || fail 1); order_prepare
-   end
- | H : ?R ?x ?y |- _ =>
-   match R with
-   | eq => fail 1
-   | lt => fail 1
-   | le => fail 1
-   | _ => (change (x==y) in H ||
-           change (x<y) in H ||
-           change (x<=y) in H ||
-           clear H || fail 1); order_prepare
-   end
- | |- ~ _ => intro; order_prepare
- | |- _ ?x ?x =>
-   exact (eq_refl x) || exact (le_refl x) || exfalso
- | _ =>
-   (apply not_neq_eq; intro) ||
-   (apply not_ge_lt; intro) ||
-   (apply not_gt_le; intro) || exfalso
- end.
-
-(** We now try to prove False from the various [< <= == !=] hypothesis *)
-
-Ltac order_loop :=
- match goal with
- (* First, successful situations *)
- | H : ?x < ?x |- _ => exact (lt_irrefl H)
- | H : ~ ?x == ?x |- _ => exact (H (eq_refl x))
- (* Second, useless hyps *)
- | H : ?x <= ?x |- _ => clear H; order_loop
- (* Third, we eliminate equalities *)
- | H : ?x == ?y |- _ => order_eq x y H; order_loop
- (* Simultaneous le and ge is eq *)
- | H1 : ?x <= ?y, H2 : ?y <= ?x |- _ =>
-     generalize (le_antisym H1 H2); clear H1 H2; intro; order_loop
- (* Simultaneous le and ~eq is lt *)
- | H1: ?x <= ?y, H2: ~ ?x == ?y |- _ =>
-     generalize (le_neq_lt H1 H2); clear H1 H2; intro; order_loop
- | H1: ?x <= ?y, H2: ~ ?y == ?x |- _ =>
-     generalize (le_neq_lt H1 (neq_sym H2)); clear H1 H2; intro; order_loop
- (* Transitivity of lt and le *)
- | H1 : ?x < ?y, H2 : ?y < ?z |- _ =>
-    match goal with
-      | H : x < z |- _ => fail 1
-      | _ => generalize (lt_trans H1 H2); intro; order_loop
-    end
- | H1 : ?x <= ?y, H2 : ?y < ?z |- _ =>
-    match goal with
-      | H : x < z |- _ => fail 1
-      | _ => generalize (le_lt_trans H1 H2); intro; order_loop
-    end
- | H1 : ?x < ?y, H2 : ?y <= ?z |- _ =>
-    match goal with
-      | H : x < z |- _ => fail 1
-      | _ => generalize (lt_le_trans H1 H2); intro; order_loop
-    end
- | H1 : ?x <= ?y, H2 : ?y <= ?z |- _ =>
-    match goal with
-      | H : x <= z |- _ => fail 1
-      | _ => generalize (le_trans H1 H2); intro; order_loop
-    end
- | _ => idtac
-end.
-
-(** The complete tactic. *)
-
-Ltac order :=
- intros; order_prepare; order_loop; fail "Order tactic unsuccessful".
-
-End MakeOrderTac.
-
-Module OTF_to_OrderTac (OTF:OrderedTypeFull).
- Module TO := OTF_to_TotalOrder OTF.
- Module TO' := CloneOrder TO.
- Include MakeOrderTac TO'.
-End OTF_to_OrderTac.
-
-Module OT_to_OrderTac (OT:OrderedType).
- Module OTF := OT_to_Full OT.
- Include OTF_to_OrderTac OTF.
-End OT_to_OrderTac.
-
-(** For example of use of this tactic, see for instance [OrderedType] *)
-
-
-Module TotalOrderRev (O:TotalOrder) <: TotalOrder.
-
-Definition t := O.t.
-Definition eq := O.eq.
-Definition lt := flip O.lt.
-Definition le := flip O.le.
-Include EqLtLeNotation.
-
-Instance eq_equiv : Equivalence eq.
-
-Instance lt_strorder: StrictOrder lt.
-Proof. unfold lt; auto with *. Qed.
-Instance lt_compat : Proper (eq==>eq==>iff) lt.
-Proof. unfold lt; auto with *. Qed.
-
-Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y.
-Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed.
-
-Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
-Proof.
- intros x y; unfold lt, eq, flip.
- generalize (O.lt_total x y); intuition.
-Qed.
-
-End TotalOrderRev.
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/OrderedType2.v
deleted file mode 100644
index 766b0faf05..0000000000
--- a/theories/Structures/OrderedType2.v
+++ /dev/null
@@ -1,160 +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 Export Relations Morphisms Setoid DecidableType2.
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-(** * Ordered types *)
-
-(** First, signatures with only the order relations *)
-
-Module Type HasLt (Import T:Typ).
-  Parameter Inline lt : t -> t -> Prop.
-End HasLt.
-
-Module Type HasLe (Import T:Typ).
-  Parameter Inline le : t -> t -> Prop.
-End HasLe.
-
-Module Type EqLt := Typ <+ HasEq <+ HasLt.
-Module Type EqLe := Typ <+ HasEq <+ HasLe.
-Module Type EqLtLe := Typ <+ HasEq <+ HasLt <+ HasLe.
-
-(** Versions with nice notations *)
-
-Module Type LtNotation (E:EqLt).
-  Infix "<" := E.lt.
-  Notation "x > y" := (y<x) (only parsing).
-  Notation "x < y < z" := (x<y /\ y<z).
-End LtNotation.
-
-Module Type LeNotation (E:EqLe).
-  Infix "<=" := E.le.
-  Notation "x >= y" := (y<=x) (only parsing).
-  Notation "x <= y <= z" := (x<=y /\ y<=z).
-End LeNotation.
-
-Module Type LtLeNotation (E:EqLtLe).
-  Include LtNotation E <+ LeNotation E.
-  Notation "x <= y < z" := (x<=y /\ y<z).
-  Notation "x < y <= z" := (x<y /\ y<=z).
-End LtLeNotation.
-
-Module Type EqLtNotation (E:EqLt) := EqNotation E <+ LtNotation E.
-Module Type EqLeNotation (E:EqLe) := EqNotation E <+ LeNotation E.
-Module Type EqLtLeNotation (E:EqLtLe) := EqNotation E <+ LtLeNotation E.
-
-Module Type EqLt' := EqLt <+ EqLtNotation.
-Module Type EqLe' := EqLe <+ EqLeNotation.
-Module Type EqLtLe' := EqLtLe <+ EqLtLeNotation.
-
-(** Versions with logical specifications *)
-
-Module Type IsStrOrder (Import E:EqLt).
-  Declare Instance lt_strorder : StrictOrder lt.
-  Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
-End IsStrOrder.
-
-Module Type LeIsLtEq (Import E:EqLtLe').
-  Axiom le_lteq : forall x y, x<=y <-> x<y \/ x==y.
-End LeIsLtEq.
-
-Module Type HasCompare (Import E:EqLt).
-  Parameter Inline compare : t -> t -> comparison.
-  Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
-End HasCompare.
-
-Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder.
-Module Type DecStrOrder := StrOrder <+ HasCompare.
-Module Type OrderedType <: DecidableType := DecStrOrder <+ HasEqDec.
-Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq.
-
-Module Type StrOrder' := StrOrder <+ EqLtNotation.
-Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation.
-Module Type OrderedType' := OrderedType <+ EqLtNotation.
-Module Type OrderedTypeFull' := OrderedTypeFull <+ EqLtLeNotation.
-
-
-(** NB: in [OrderedType], an [eq_dec] could be deduced from [compare].
-  But adding this redundant field allows to see an [OrderedType] as a
-  [DecidableType]. *)
-
-(** * Versions with [eq] being the usual Leibniz equality of Coq *)
-
-Module Type UsualStrOrder := UsualEqualityType <+ HasLt <+ IsStrOrder.
-Module Type UsualDecStrOrder := UsualStrOrder <+ HasCompare.
-Module Type UsualOrderedType <: UsualDecidableType <: OrderedType
- := UsualDecStrOrder <+ HasEqDec.
-Module Type UsualOrderedTypeFull := UsualOrderedType <+ HasLe <+ LeIsLtEq.
-
-(** NB: in [UsualOrderedType], the field [lt_compat] is
-    useless since [eq] is [Leibniz], but it should be
-    there for subtyping. *)
-
-Module Type UsualStrOrder' := UsualStrOrder <+ LtNotation.
-Module Type UsualDecStrOrder' := UsualDecStrOrder <+ LtNotation.
-Module Type UsualOrderedType' := UsualOrderedType <+ LtNotation.
-Module Type UsualOrderedTypeFull' := UsualOrderedTypeFull <+ LtLeNotation.
-
-(** * Purely logical versions *)
-
-Module Type LtIsTotal (Import E:EqLt').
-  Axiom lt_total : forall x y, x<y \/ x==y \/ y<x.
-End LtIsTotal.
-
-Module Type TotalOrder := StrOrder <+ HasLe <+ LeIsLtEq <+ LtIsTotal.
-Module Type UsualTotalOrder <: TotalOrder
- := UsualStrOrder <+ HasLe <+ LeIsLtEq <+ LtIsTotal.
-
-Module Type TotalOrder' := TotalOrder <+ EqLtLeNotation.
-Module Type UsualTotalOrder' := UsualTotalOrder <+ LtLeNotation.
-
-(** * Conversions *)
-
-(** From [compare] to [eqb], and then [eq_dec] *)
-
-Module Compare2EqBool (Import O:DecStrOrder') <: HasEqBool O.
-
- Definition eqb x y :=
-   match compare x y with Eq => true | _ => false end.
-
- Lemma eqb_eq : forall x y, eqb x y = true <-> x==y.
- Proof.
- unfold eqb. intros x y.
- destruct (compare_spec x y) as [H|H|H]; split; auto; try discriminate.
- intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H).
- intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H).
- Qed.
-
-End Compare2EqBool.
-
-Module DSO_to_OT (O:DecStrOrder) <: OrderedType :=
-  O <+ Compare2EqBool <+ HasEqBool2Dec.
-
-(** From [OrderedType] To [OrderedTypeFull] (adding [<=]) *)
-
-Module OT_to_Full (O:OrderedType') <: OrderedTypeFull.
- Include O.
- Definition le x y := x<y \/ x==y.
- Lemma le_lteq : forall x y, le x y <-> x<y \/ x==y.
- Proof. unfold le; split; auto. Qed.
-End OT_to_Full.
-
-(** From computational to logical versions *)
-
-Module OTF_LtIsTotal (Import O:OrderedTypeFull') <: LtIsTotal O.
- Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
- Proof. intros; destruct (compare_spec x y); auto. Qed.
-End OTF_LtIsTotal.
-
-Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder
- := O <+ OTF_LtIsTotal.
-
diff --git a/theories/Structures/OrderedType2Alt.v b/theories/Structures/OrderedType2Alt.v
deleted file mode 100644
index b036b50e5b..0000000000
--- a/theories/Structures/OrderedType2Alt.v
+++ /dev/null
@@ -1,243 +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       *)
-(***********************************************************************)
-
-(* Finite sets library.
- * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
- * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
- *              91405 Orsay, France *)
-
-(* $Id$ *)
-
-Require Import OrderedType OrderedType2.
-Set Implicit Arguments.
-
-(** * Some alternative (but equivalent) presentations for an Ordered Type
-   inferface. *)
-
-(** ** The original interface *)
-
-Module Type OrderedTypeOrig := OrderedType.OrderedType.
-
-(** ** An interface based on compare *)
-
-Module Type OrderedTypeAlt.
-
- Parameter t : Type.
-
- Parameter compare : t -> t -> comparison.
-
- Infix "?=" := compare (at level 70, no associativity).
-
- Parameter compare_sym :
-   forall x y, (y?=x) = CompOpp (x?=y).
- Parameter compare_trans :
-   forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
-
-End OrderedTypeAlt.
-
-(** ** From OrderedTypeOrig to OrderedType. *)
-
-Module Update_OT (O:OrderedTypeOrig) <: OrderedType.
-
- Include Update_DT O.  (* Provides : t eq eq_equiv eq_dec *)
-
- Definition lt := O.lt.
-
- Instance lt_strorder : StrictOrder lt.
- Proof.
-  split.
-  intros x Hx. apply (O.lt_not_eq Hx); auto with *.
-  exact O.lt_trans.
- Qed.
-
- Instance lt_compat : Proper (eq==>eq==>iff) lt.
- Proof.
-  apply proper_sym_impl_iff_2; auto with *.
-  intros x x' Hx y y' Hy H.
-  assert (H0 : lt x' y).
-   destruct (O.compare x' y) as [H'|H'|H']; auto.
-   elim (O.lt_not_eq H). transitivity x'; auto with *.
-   elim (O.lt_not_eq (O.lt_trans H H')); auto.
-  destruct (O.compare x' y') as [H'|H'|H']; auto.
-  elim (O.lt_not_eq H).
-   transitivity x'; auto with *. transitivity y'; auto with *.
-  elim (O.lt_not_eq (O.lt_trans H' H0)); auto with *.
- Qed.
-
- Definition compare x y :=
-   match O.compare x y with
-    | EQ _ => Eq
-    | LT _ => Lt
-    | GT _ => Gt
-  end.
-
- Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
- Proof.
-  intros; unfold compare; destruct O.compare; auto.
- Qed.
-
-End Update_OT.
-
-(** ** From OrderedType to OrderedTypeOrig. *)
-
-Module Backport_OT (O:OrderedType) <: OrderedTypeOrig.
-
- Include Backport_DT O. (* Provides : t eq eq_refl eq_sym eq_trans eq_dec *)
-
- Definition lt := O.lt.
-
- Lemma lt_not_eq : forall x y, lt x y -> ~eq x y.
- Proof.
-  intros x y L E; rewrite E in L. apply (StrictOrder_Irreflexive y); auto.
- Qed.
-
- Lemma lt_trans : Transitive lt.
- Proof. apply O.lt_strorder. Qed.
-
- Definition compare : forall x y, Compare lt eq x y.
- Proof.
-  intros. assert (H:=O.compare_spec x y).
-  destruct (O.compare x y); [apply EQ|apply LT|apply GT];
-   inversion H; auto.
- Defined.
-
-End Backport_OT.
-
-
-(** ** From OrderedTypeAlt to OrderedType. *)
-
-Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
-
- Definition t := t.
-
- Definition eq x y := (x?=y) = Eq.
- Definition lt x y := (x?=y) = Lt.
-
- Instance eq_equiv : Equivalence eq.
- Proof.
-  split; red.
-  (* refl *)
-  unfold eq; intros x.
-  assert (H:=compare_sym x x).
-  destruct (x ?= x); simpl in *; auto; discriminate.
-  (* sym *)
-  unfold eq; intros x y H.
-  rewrite compare_sym, H; simpl; auto.
-  (* trans *)
-  apply compare_trans.
- Qed.
-
- Instance lt_strorder : StrictOrder lt.
- Proof.
-  split; repeat red; unfold lt; try apply compare_trans.
-  intros x H.
-  assert (eq x x) by reflexivity.
-  unfold eq in *; congruence.
- Qed.
-
- Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.
- Proof.
-  unfold lt, eq; intros x y z Hxy Hyz.
-  destruct (compare x z) as [ ]_eqn:Hxz; auto.
-  rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz.
-  rewrite (compare_trans Hxz Hyz) in Hxy; discriminate.
-  rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy.
-  rewrite (compare_trans Hxy Hxz) in Hyz; discriminate.
- Qed.
-
- Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z.
- Proof.
-  unfold lt, eq; intros x y z Hxy Hyz.
-  destruct (compare x z) as [ ]_eqn:Hxz; auto.
-  rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy.
-  rewrite (compare_trans Hxy Hxz) in Hyz; discriminate.
-  rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz.
-  rewrite (compare_trans Hxz Hyz) in Hxy; discriminate.
- Qed.
-
- Instance lt_compat : Proper (eq==>eq==>iff) lt.
- Proof.
-  apply proper_sym_impl_iff_2; auto with *.
-  repeat red; intros.
-  eapply lt_eq; eauto. eapply eq_lt; eauto. symmetry; auto.
- Qed.
-
- Definition compare := O.compare.
-
- Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
- Proof.
-  unfold eq, lt, compare; intros.
-  destruct (O.compare x y) as [ ]_eqn:H; auto.
-  apply CompGt.
-  rewrite compare_sym, H; auto.
- Qed.
-
- 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 OT_from_Alt.
-
-(** From the original presentation to this alternative one. *)
-
-Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt.
-
- Definition t := t.
- Definition compare := compare.
-
- Infix "?=" := compare (at level 70, no associativity).
-
- Lemma compare_sym :
-   forall x y, (y?=x) = CompOpp (x?=y).
- Proof.
- intros x y; unfold compare.
- destruct (compare_spec x y) as [U|U|U];
-  destruct (compare_spec y x) as [V|V|V]; auto.
- rewrite U in V. elim (StrictOrder_Irreflexive y); auto.
- rewrite U in V. elim (StrictOrder_Irreflexive y); auto.
- rewrite V in U. elim (StrictOrder_Irreflexive x); auto.
- rewrite V in U. elim (StrictOrder_Irreflexive x); auto.
- rewrite V in U. elim (StrictOrder_Irreflexive x); auto.
- rewrite V in U. elim (StrictOrder_Irreflexive y); auto.
- Qed.
-
- Lemma compare_Eq : forall x y, compare x y = Eq <-> eq x y.
- Proof.
- unfold compare.
- intros x y; destruct (compare_spec x y); intuition;
-  try discriminate.
- rewrite H0 in H. elim (StrictOrder_Irreflexive y); auto.
- rewrite H0 in H. elim (StrictOrder_Irreflexive y); auto.
- Qed.
-
- Lemma compare_Lt : forall x y, compare x y = Lt <-> lt x y.
- Proof.
- unfold compare.
- intros x y; destruct (compare_spec x y); intuition;
-  try discriminate.
- rewrite H in H0. elim (StrictOrder_Irreflexive y); auto.
- rewrite H in H0. elim (StrictOrder_Irreflexive x); auto.
- Qed.
-
- Lemma compare_Gt : forall x y, compare x y = Gt <-> lt y x.
- Proof.
- intros x y. rewrite compare_sym, CompOpp_iff. apply compare_Lt.
- Qed.
-
- Lemma compare_trans :
-   forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
- Proof.
- intros c x y z.
- destruct c; unfold compare;
-  rewrite ?compare_Eq, ?compare_Lt, ?compare_Gt;
-  transitivity y; auto.
- Qed.
-
-End OT_to_Alt.
diff --git a/theories/Structures/OrderedType2Ex.v b/theories/Structures/OrderedType2Ex.v
deleted file mode 100644
index 1e45a3fbfb..0000000000
--- a/theories/Structures/OrderedType2Ex.v
+++ /dev/null
@@ -1,88 +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       *)
-(***********************************************************************)
-
-(* Finite sets library.
- * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
- * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
- *              91405 Orsay, France *)
-
-(* $Id$ *)
-
-Require Import OrderedType2 NatOrderedType POrderedType NOrderedType
- ZOrderedType DecidableType2Ex RelationPairs.
-
-(** * Examples of Ordered Type structures. *)
-
-
-(** Ordered Type for [nat], [Positive], [N], [Z] with the usual order. *)
-
-Module Nat_as_OT := NatOrderedType.Nat_as_OT.
-Module Positive_as_OT := POrderedType.Positive_as_OT.
-Module N_as_OT := NOrderedType.N_as_OT.
-Module Z_as_OT := ZOrderedType.Z_as_OT.
-
-(** 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 := 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 ordered types, we can build a new OrderedType
-   over their cartesian product, using the lexicographic order. *)
-
-Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
- Include PairDecidableType O1 O2.
-
- Definition lt :=
-   (relation_disjunction (O1.lt @@1) (O1.eq * O2.lt))%signature.
-
- Instance lt_strorder : StrictOrder lt.
- Proof.
- split.
- (* irreflexive *)
- intros (x1,x2); compute. destruct 1.
- apply (StrictOrder_Irreflexive x1); auto.
- apply (StrictOrder_Irreflexive x2); intuition.
- (* transitive *)
- intros (x1,x2) (y1,y2) (z1,z2). compute. intuition.
- left; etransitivity; eauto.
- left. setoid_replace z1 with y1; auto with relations.
- left; setoid_replace x1 with y1; auto with relations.
- right; split; etransitivity; eauto.
- Qed.
-
- Instance lt_compat : Proper (eq==>eq==>iff) lt.
- Proof.
- compute.
- intros (x1,x2) (x1',x2') (X1,X2) (y1,y2) (y1',y2') (Y1,Y2).
- rewrite X1,X2,Y1,Y2; intuition.
- Qed.
-
- Definition compare x y :=
-  match O1.compare (fst x) (fst y) with
-   | Eq => O2.compare (snd x) (snd y)
-   | Lt => Lt
-   | Gt => Gt
-  end.
-
- Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
- Proof.
- intros (x1,x2) (y1,y2); unfold compare; simpl.
- destruct (O1.compare_spec x1 y1); try (constructor; compute; auto).
- destruct (O2.compare_spec x2 y2); constructor; compute; auto with relations.
- Qed.
-
-End PairOrderedType.
-
diff --git a/theories/Structures/OrderedType2Facts.v b/theories/Structures/OrderedType2Facts.v
deleted file mode 100644
index b5dc0c92fc..0000000000
--- a/theories/Structures/OrderedType2Facts.v
+++ /dev/null
@@ -1,234 +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       *)
-(***********************************************************************)
-
-Require Import Basics OrderTac.
-Require Export OrderedType2.
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-(** * Properties of [OrderedTypeFull] *)
-
-Module OrderedTypeFullFacts (Import O:OrderedTypeFull').
-
- Module OrderTac := OTF_to_OrderTac O.
- Ltac order := OrderTac.order.
- Ltac iorder := intuition order.
-
- Instance le_compat : Proper (eq==>eq==>iff) le.
- Proof. repeat red; iorder. Qed.
-
- Instance le_preorder : PreOrder le.
- Proof. split; red; order. Qed.
-
- Instance le_order : PartialOrder eq le.
- Proof. compute; iorder. Qed.
-
- Instance le_antisym : Antisymmetric _ eq le.
- Proof. apply partial_order_antisym; auto with *. Qed.
-
- Lemma le_not_gt_iff : forall x y, x<=y <-> ~y<x.
- Proof. iorder. Qed.
-
- Lemma lt_not_ge_iff : forall x y, x<y <-> ~y<=x.
- Proof. iorder. Qed.
-
- Lemma le_or_gt : forall x y, x<=y \/ y<x.
- Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed.
-
- Lemma lt_or_ge : forall x y, x<y \/ y<=x.
- Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); iorder. Qed.
-
- Lemma eq_is_le_ge : forall x y, x==y <-> x<=y /\ y<=x.
- Proof. iorder. Qed.
-
-End OrderedTypeFullFacts.
-
-
-(** * Properties of [OrderedType] *)
-
-Module OrderedTypeFacts (Import O: OrderedType').
-
-  Module OrderTac := OT_to_OrderTac O.
-  Ltac order := OrderTac.order.
-
-  Notation "x <= y" := (~lt y x) : order.
-  Infix "?=" := compare (at level 70, no associativity) : order.
-
-  Local Open Scope order.
-
-  Tactic Notation "elim_compare" constr(x) constr(y) :=
-   destruct (compare_spec x y).
-
-  Tactic Notation "elim_compare" constr(x) constr(y) "as" ident(h) :=
-   destruct (compare_spec x y) as [h|h|h].
-
-  (** The following lemmas are either re-phrasing of [eq_equiv] and
-      [lt_strorder] or immediately provable by [order]. Interest:
-      compatibility, test of order, etc *)
-
-  Definition eq_refl (x:t) : x==x := Equivalence_Reflexive x.
-
-  Definition eq_sym (x y:t) : x==y -> y==x := Equivalence_Symmetric x y.
-
-  Definition eq_trans (x y z:t) : x==y -> y==z -> x==z :=
-   Equivalence_Transitive x y z.
-
-  Definition lt_trans (x y z:t) : x<y -> y<z -> x<z :=
-   StrictOrder_Transitive x y z.
-
-  Definition lt_irrefl (x:t) : ~x<x := StrictOrder_Irreflexive x.
-
-  (** Some more about [compare] *)
-
-  Lemma compare_eq_iff : forall x y, (x ?= y) = Eq <-> x==y.
-  Proof.
-   intros; elim_compare x y; intuition; try discriminate; order.
-  Qed.
-
-  Lemma compare_lt_iff : forall x y, (x ?= y) = Lt <-> x<y.
-  Proof.
-   intros; elim_compare x y; intuition; try discriminate; order.
-  Qed.
-
-  Lemma compare_gt_iff : forall x y, (x ?= y) = Gt <-> y<x.
-  Proof.
-   intros; elim_compare x y; intuition; try discriminate; order.
-  Qed.
-
-  Lemma compare_ge_iff : forall x y, (x ?= y) <> Lt <-> y<=x.
-  Proof.
-   intros; rewrite compare_lt_iff; intuition.
-  Qed.
-
-  Lemma compare_le_iff : forall x y, (x ?= y) <> Gt <-> x<=y.
-  Proof.
-   intros; rewrite compare_gt_iff; intuition.
-  Qed.
-
-  Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.
-
-  Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare.
-  Proof.
-  intros x x' Hxx' y y' Hyy'.
-  elim_compare x' y'; autorewrite with order; order.
-  Qed.
-
-  Lemma compare_refl : forall x, (x ?= x) = Eq.
-  Proof.
-   intros; elim_compare x x; auto; order.
-  Qed.
-
-  Lemma compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y).
-  Proof.
-   intros; elim_compare x y; simpl; autorewrite with order; order.
-  Qed.
-
-  (** For compatibility reasons *)
-  Definition eq_dec := eq_dec.
-
-  Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}.
-  Proof.
-   intros; assert (H:=compare_spec x y); destruct (compare x y);
-    [ right | left | right ]; inversion_clear H; order.
-  Defined.
-
-  Definition eqb x y : bool := if eq_dec x y then true else false.
-
-  Lemma if_eq_dec : forall x y (B:Type)(b b':B),
-    (if eq_dec x y then b else b') =
-    (match compare x y with Eq => b | _ => b' end).
-  Proof.
-  intros; destruct eq_dec; elim_compare x y; auto; order.
-  Qed.
-
-  Lemma eqb_alt :
-    forall x y, eqb x y = match compare x y with Eq => true | _ => false end.
-  Proof.
-  unfold eqb; intros; apply if_eq_dec.
-  Qed.
-
-  Instance eqb_compat : Proper (eq==>eq==>Logic.eq) eqb.
-  Proof.
-  intros x x' Hxx' y y' Hyy'.
-  rewrite 2 eqb_alt, Hxx', Hyy'; auto.
-  Qed.
-
-End OrderedTypeFacts.
-
-
-
-
-
-
-(** * Tests of the order tactic
-
-    Is it at least capable of proving some basic properties ? *)
-
-Module OrderedTypeTest (Import O:OrderedType').
-  Module Import MO := OrderedTypeFacts O.
-  Local Open Scope order.
-  Lemma lt_not_eq x y : x<y -> ~x==y.  Proof. order. Qed.
-  Lemma lt_eq x y z : x<y -> y==z -> x<z. Proof. order. Qed.
-  Lemma eq_lt x y z : x==y -> y<z -> x<z. Proof. order. Qed.
-  Lemma le_eq x y z : x<=y -> y==z -> x<=z. Proof. order. Qed.
-  Lemma eq_le x y z : x==y -> y<=z -> x<=z. Proof. order. Qed.
-  Lemma neq_eq x y z : ~x==y -> y==z -> ~x==z. Proof. order. Qed.
-  Lemma eq_neq x y z : x==y -> ~y==z -> ~x==z. Proof. order. Qed.
-  Lemma le_lt_trans x y z : x<=y -> y<z -> x<z. Proof. order. Qed.
-  Lemma lt_le_trans x y z : x<y -> y<=z -> x<z. Proof. order. Qed.
-  Lemma le_trans x y z : x<=y -> y<=z -> x<=z. Proof. order. Qed.
-  Lemma le_antisym x y : x<=y -> y<=x -> x==y. Proof. order. Qed.
-  Lemma le_neq x y : x<=y -> ~x==y -> x<y. Proof. order. Qed.
-  Lemma neq_sym x y : ~x==y -> ~y==x. Proof. order. Qed.
-  Lemma lt_le x y : x<y -> x<=y. Proof. order. Qed.
-  Lemma gt_not_eq x y : y<x -> ~x==y. Proof. order. Qed.
-  Lemma eq_not_lt x y : x==y -> ~x<y. Proof. order. Qed.
-  Lemma eq_not_gt x y : x==y -> ~ y<x. Proof. order. Qed.
-  Lemma lt_not_gt x y : x<y -> ~ y<x. Proof. order. Qed.
-  Lemma eq_is_nlt_ngt x y : x==y <-> ~x<y /\ ~y<x.
-  Proof. intuition; order. Qed.
-End OrderedTypeTest.
-
-
-
-(** * Reversed OrderedTypeFull.
-
-   we can switch the orientation of the order. This is used for
-   example when deriving properties of [min] out of the ones of [max]
-   (see [GenericMinMax]).
-*)
-
-Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull.
-
-Definition t := O.t.
-Definition eq := O.eq.
-Instance eq_equiv : Equivalence eq.
-Definition eq_dec := O.eq_dec.
-
-Definition lt := flip O.lt.
-Definition le := flip O.le.
-
-Instance lt_strorder: StrictOrder lt.
-Proof. unfold lt; auto with *. Qed.
-Instance lt_compat : Proper (eq==>eq==>iff) lt.
-Proof. unfold lt; auto with *. Qed.
-
-Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
-Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed.
-
-Definition compare := flip O.compare.
-
-Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
-Proof.
-intros; unfold compare, eq, lt, flip.
-destruct (O.compare_spec y x); auto with relations.
-Qed.
-
-End OrderedTypeRev.
-
diff --git a/theories/Structures/OrderedType2Lists.v b/theories/Structures/OrderedType2Lists.v
deleted file mode 100644
index 79690fb024..0000000000
--- a/theories/Structures/OrderedType2Lists.v
+++ /dev/null
@@ -1,256 +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       *)
-(***********************************************************************)
-
-Require Export RelationPairs SetoidList OrderedType2.
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-(** * Specialization of results about lists modulo. *)
-
-Module OrderedTypeLists (Import O:OrderedType).
-
-Section ForNotations.
-
-Notation In:=(InA eq).
-Notation Inf:=(lelistA lt).
-Notation Sort:=(sort lt).
-Notation NoDup:=(NoDupA eq).
-
-Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
-Proof. intros. rewrite <- H; auto. Qed.
-
-Lemma ListIn_In : forall l x, List.In x l -> In x l.
-Proof. exact (In_InA eq_equiv). Qed.
-
-Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_ltA lt_strorder). Qed.
-
-Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed.
-
-Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x.
-Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed.
-
-Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> lt x y) -> Inf x l.
-Proof. exact (@In_InfA t lt). Qed.
-
-Lemma In_Inf : forall l x, (forall y, In y l -> lt x y) -> Inf x l.
-Proof. exact (InA_InfA eq_equiv (ltA:=lt)). Qed.
-
-Lemma Inf_alt :
- forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)).
-Proof. exact (InfA_alt eq_equiv lt_strorder lt_compat). Qed.
-
-Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
-Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat) . Qed.
-
-End ForNotations.
-
-Hint Resolve ListIn_In Sort_NoDup Inf_lt.
-Hint Immediate In_eq Inf_lt.
-
-End OrderedTypeLists.
-
-
-
-
-
-(** * Results about keys and data as manipulated in FMaps. *)
-
-
-Module KeyOrderedType(Import O:OrderedType).
- Module Import MO:=OrderedTypeLists(O).
-
- Section Elt.
- Variable elt : Type.
- Notation key:=t.
-
-  Local Open Scope signature_scope.
-
-  Definition eqk : relation (key*elt) := eq @@1.
-  Definition eqke : relation (key*elt) := eq * Logic.eq.
-  Definition ltk : relation (key*elt) := lt @@1.
-
-  Hint Unfold eqk eqke ltk.
-
-  (* eqke is stricter than eqk *)
-
-  Global Instance eqke_eqk : subrelation eqke eqk.
-  Proof. firstorder. Qed.
-
-  (* eqk, eqke are equalities, ltk is a strict order *)
-
-  Global Instance eqk_equiv : Equivalence eqk.
-
-  Global Instance eqke_equiv : Equivalence eqke.
-
-  Global Instance ltk_strorder : StrictOrder ltk.
-
-  Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
-  Proof. unfold eqk, ltk; auto with *. Qed.
-
-  (* Additionnal facts *)
-
-  Global Instance pair_compat : Proper (eq==>Logic.eq==>eqke) (@pair key elt).
-  Proof. apply pair_compat. Qed.
-
-  Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'.
-  Proof.
-  intros e e' LT EQ; rewrite EQ in LT.
-  elim (StrictOrder_Irreflexive _ LT).
-  Qed.
-
-  Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'.
-  Proof.
-  intros e e' LT EQ; rewrite EQ in LT.
-  elim (StrictOrder_Irreflexive _ LT).
-  Qed.
-
-  Lemma InA_eqke_eqk :
-     forall x m, InA eqke x m -> InA eqk x m.
-  Proof.
-    unfold eqke, RelProd; induction 1; firstorder.
-  Qed.
-  Hint Resolve InA_eqke_eqk.
-
-  Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
-  Definition In k m := exists e:elt, MapsTo k e m.
-  Notation Sort := (sort ltk).
-  Notation Inf := (lelistA ltk).
-
-  Hint Unfold MapsTo In.
-
-  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
-
-  Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
-  Proof.
-  firstorder.
-  exists x; auto.
-  induction H.
-  destruct y; compute in H.
-  exists e; left; auto.
-  destruct IHInA as [e H0].
-  exists e; auto.
-  Qed.
-
-  Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l.
-  Proof.
-  unfold In, MapsTo.
-  setoid_rewrite Exists_exists; setoid_rewrite InA_alt.
-  firstorder.
-  exists (snd x), x; auto.
-  Qed.
-
-  Lemma In_nil : forall k, In k nil <-> False.
-  Proof.
-  intros; rewrite In_alt2; apply Exists_nil.
-  Qed.
-
-  Lemma In_cons : forall k p l,
-   In k (p::l) <-> eq k (fst p) \/ In k l.
-  Proof.
-  intros; rewrite !In_alt2, Exists_cons; intuition.
-  Qed.
-
-  Global Instance MapsTo_compat :
-   Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo.
-  Proof.
-  intros x x' Hx e e' He l l' Hl. unfold MapsTo.
-  rewrite Hx, He, Hl; intuition.
-  Qed.
-
-  Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In.
-  Proof.
-  intros x x' Hx l l' Hl. rewrite !In_alt.
-  setoid_rewrite Hl. setoid_rewrite Hx. intuition.
-  Qed.
-
-  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
-  Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed.
-
-  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
-  Proof. intros l x y EQ. rewrite <- EQ; auto. Qed.
-
-  Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.
-  Proof. intros l x x' H. rewrite H; auto. Qed.
-
-  Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
-  Proof. apply InfA_ltA; auto with *. Qed.
-
-  Hint Immediate Inf_eq.
-  Hint Resolve Inf_lt.
-
-  Lemma Sort_Inf_In :
-      forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p.
-  Proof. apply SortA_InfA_InA; auto with *. Qed.
-
-  Lemma Sort_Inf_NotIn :
-      forall l k e, Sort l -> Inf (k,e) l ->  ~In k l.
-  Proof.
-    intros; red; intros.
-    destruct H1 as [e' H2].
-    elim (@ltk_not_eqk (k,e) (k,e')).
-    eapply Sort_Inf_In; eauto.
-    repeat red; reflexivity.
-  Qed.
-
-  Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l.
-  Proof. apply SortA_NoDupA; auto with *. Qed.
-
-  Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'.
-  Proof.
-   intros; invlist sort; eapply Sort_Inf_In; eauto.
-  Qed.
-
-  Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) ->
-      ltk e e' \/ eqk e e'.
-  Proof.
-    intros; invlist InA; auto with relations.
-    left; apply Sort_In_cons_1 with l; auto with relations.
-  Qed.
-
-  Lemma Sort_In_cons_3 :
-    forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k.
-  Proof.
-    intros; invlist sort; red; intros.
-    eapply Sort_Inf_NotIn; eauto using In_eq.
-  Qed.
-
-  Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
-  Proof.
-    intros; invlist In; invlist MapsTo. compute in * |- ; intuition.
-    right; exists x; auto.
-  Qed.
-
-  Lemma In_inv_2 : forall k k' e e' l,
-      InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
-  Proof.
-   intros; invlist InA; intuition.
-  Qed.
-
-  Lemma In_inv_3 : forall x x' l,
-      InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
-  Proof.
-   intros; invlist InA; compute in * |- ; intuition.
-  Qed.
-
- End Elt.
-
- Hint Unfold eqk eqke ltk.
- Hint Extern 2 (eqke ?a ?b) => split.
- Hint Resolve ltk_not_eqk ltk_not_eqke.
- Hint Resolve InA_eqke_eqk.
- Hint Unfold MapsTo In.
- Hint Immediate Inf_eq.
- Hint Resolve Inf_lt.
- Hint Resolve Sort_Inf_NotIn.
- Hint Resolve In_inv_2 In_inv_3.
-
-End KeyOrderedType.
-
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
new file mode 100644
index 0000000000..c71be0a6ee
--- /dev/null
+++ b/theories/Structures/Orders.v
@@ -0,0 +1,160 @@
+(***********************************************************************)
+(*  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 Export Relations Morphisms Setoid Equalities.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Ordered types *)
+
+(** First, signatures with only the order relations *)
+
+Module Type HasLt (Import T:Typ).
+  Parameter Inline lt : t -> t -> Prop.
+End HasLt.
+
+Module Type HasLe (Import T:Typ).
+  Parameter Inline le : t -> t -> Prop.
+End HasLe.
+
+Module Type EqLt := Typ <+ HasEq <+ HasLt.
+Module Type EqLe := Typ <+ HasEq <+ HasLe.
+Module Type EqLtLe := Typ <+ HasEq <+ HasLt <+ HasLe.
+
+(** Versions with nice notations *)
+
+Module Type LtNotation (E:EqLt).
+  Infix "<" := E.lt.
+  Notation "x > y" := (y<x) (only parsing).
+  Notation "x < y < z" := (x<y /\ y<z).
+End LtNotation.
+
+Module Type LeNotation (E:EqLe).
+  Infix "<=" := E.le.
+  Notation "x >= y" := (y<=x) (only parsing).
+  Notation "x <= y <= z" := (x<=y /\ y<=z).
+End LeNotation.
+
+Module Type LtLeNotation (E:EqLtLe).
+  Include LtNotation E <+ LeNotation E.
+  Notation "x <= y < z" := (x<=y /\ y<z).
+  Notation "x < y <= z" := (x<y /\ y<=z).
+End LtLeNotation.
+
+Module Type EqLtNotation (E:EqLt) := EqNotation E <+ LtNotation E.
+Module Type EqLeNotation (E:EqLe) := EqNotation E <+ LeNotation E.
+Module Type EqLtLeNotation (E:EqLtLe) := EqNotation E <+ LtLeNotation E.
+
+Module Type EqLt' := EqLt <+ EqLtNotation.
+Module Type EqLe' := EqLe <+ EqLeNotation.
+Module Type EqLtLe' := EqLtLe <+ EqLtLeNotation.
+
+(** Versions with logical specifications *)
+
+Module Type IsStrOrder (Import E:EqLt).
+  Declare Instance lt_strorder : StrictOrder lt.
+  Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
+End IsStrOrder.
+
+Module Type LeIsLtEq (Import E:EqLtLe').
+  Axiom le_lteq : forall x y, x<=y <-> x<y \/ x==y.
+End LeIsLtEq.
+
+Module Type HasCompare (Import E:EqLt).
+  Parameter Inline compare : t -> t -> comparison.
+  Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+End HasCompare.
+
+Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder.
+Module Type DecStrOrder := StrOrder <+ HasCompare.
+Module Type OrderedType <: DecidableType := DecStrOrder <+ HasEqDec.
+Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq.
+
+Module Type StrOrder' := StrOrder <+ EqLtNotation.
+Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation.
+Module Type OrderedType' := OrderedType <+ EqLtNotation.
+Module Type OrderedTypeFull' := OrderedTypeFull <+ EqLtLeNotation.
+
+
+(** NB: in [OrderedType], an [eq_dec] could be deduced from [compare].
+  But adding this redundant field allows to see an [OrderedType] as a
+  [DecidableType]. *)
+
+(** * Versions with [eq] being the usual Leibniz equality of Coq *)
+
+Module Type UsualStrOrder := UsualEqualityType <+ HasLt <+ IsStrOrder.
+Module Type UsualDecStrOrder := UsualStrOrder <+ HasCompare.
+Module Type UsualOrderedType <: UsualDecidableType <: OrderedType
+ := UsualDecStrOrder <+ HasEqDec.
+Module Type UsualOrderedTypeFull := UsualOrderedType <+ HasLe <+ LeIsLtEq.
+
+(** NB: in [UsualOrderedType], the field [lt_compat] is
+    useless since [eq] is [Leibniz], but it should be
+    there for subtyping. *)
+
+Module Type UsualStrOrder' := UsualStrOrder <+ LtNotation.
+Module Type UsualDecStrOrder' := UsualDecStrOrder <+ LtNotation.
+Module Type UsualOrderedType' := UsualOrderedType <+ LtNotation.
+Module Type UsualOrderedTypeFull' := UsualOrderedTypeFull <+ LtLeNotation.
+
+(** * Purely logical versions *)
+
+Module Type LtIsTotal (Import E:EqLt').
+  Axiom lt_total : forall x y, x<y \/ x==y \/ y<x.
+End LtIsTotal.
+
+Module Type TotalOrder := StrOrder <+ HasLe <+ LeIsLtEq <+ LtIsTotal.
+Module Type UsualTotalOrder <: TotalOrder
+ := UsualStrOrder <+ HasLe <+ LeIsLtEq <+ LtIsTotal.
+
+Module Type TotalOrder' := TotalOrder <+ EqLtLeNotation.
+Module Type UsualTotalOrder' := UsualTotalOrder <+ LtLeNotation.
+
+(** * Conversions *)
+
+(** From [compare] to [eqb], and then [eq_dec] *)
+
+Module Compare2EqBool (Import O:DecStrOrder') <: HasEqBool O.
+
+ Definition eqb x y :=
+   match compare x y with Eq => true | _ => false end.
+
+ Lemma eqb_eq : forall x y, eqb x y = true <-> x==y.
+ Proof.
+ unfold eqb. intros x y.
+ destruct (compare_spec x y) as [H|H|H]; split; auto; try discriminate.
+ intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H).
+ intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H).
+ Qed.
+
+End Compare2EqBool.
+
+Module DSO_to_OT (O:DecStrOrder) <: OrderedType :=
+  O <+ Compare2EqBool <+ HasEqBool2Dec.
+
+(** From [OrderedType] To [OrderedTypeFull] (adding [<=]) *)
+
+Module OT_to_Full (O:OrderedType') <: OrderedTypeFull.
+ Include O.
+ Definition le x y := x<y \/ x==y.
+ Lemma le_lteq : forall x y, le x y <-> x<y \/ x==y.
+ Proof. unfold le; split; auto. Qed.
+End OT_to_Full.
+
+(** From computational to logical versions *)
+
+Module OTF_LtIsTotal (Import O:OrderedTypeFull') <: LtIsTotal O.
+ Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
+ Proof. intros; destruct (compare_spec x y); auto. Qed.
+End OTF_LtIsTotal.
+
+Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder
+ := O <+ OTF_LtIsTotal.
+
diff --git a/theories/Structures/OrdersAlt.v b/theories/Structures/OrdersAlt.v
new file mode 100644
index 0000000000..261e75e1c5
--- /dev/null
+++ b/theories/Structures/OrdersAlt.v
@@ -0,0 +1,243 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(* Finite sets library.
+ * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
+ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id$ *)
+
+Require Import OrderedType Orders.
+Set Implicit Arguments.
+
+(** * Some alternative (but equivalent) presentations for an Ordered Type
+   inferface. *)
+
+(** ** The original interface *)
+
+Module Type OrderedTypeOrig := OrderedType.OrderedType.
+
+(** ** An interface based on compare *)
+
+Module Type OrderedTypeAlt.
+
+ Parameter t : Type.
+
+ Parameter compare : t -> t -> comparison.
+
+ Infix "?=" := compare (at level 70, no associativity).
+
+ Parameter compare_sym :
+   forall x y, (y?=x) = CompOpp (x?=y).
+ Parameter compare_trans :
+   forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
+
+End OrderedTypeAlt.
+
+(** ** From OrderedTypeOrig to OrderedType. *)
+
+Module Update_OT (O:OrderedTypeOrig) <: OrderedType.
+
+ Include Update_DT O.  (* Provides : t eq eq_equiv eq_dec *)
+
+ Definition lt := O.lt.
+
+ Instance lt_strorder : StrictOrder lt.
+ Proof.
+  split.
+  intros x Hx. apply (O.lt_not_eq Hx); auto with *.
+  exact O.lt_trans.
+ Qed.
+
+ Instance lt_compat : Proper (eq==>eq==>iff) lt.
+ Proof.
+  apply proper_sym_impl_iff_2; auto with *.
+  intros x x' Hx y y' Hy H.
+  assert (H0 : lt x' y).
+   destruct (O.compare x' y) as [H'|H'|H']; auto.
+   elim (O.lt_not_eq H). transitivity x'; auto with *.
+   elim (O.lt_not_eq (O.lt_trans H H')); auto.
+  destruct (O.compare x' y') as [H'|H'|H']; auto.
+  elim (O.lt_not_eq H).
+   transitivity x'; auto with *. transitivity y'; auto with *.
+  elim (O.lt_not_eq (O.lt_trans H' H0)); auto with *.
+ Qed.
+
+ Definition compare x y :=
+   match O.compare x y with
+    | EQ _ => Eq
+    | LT _ => Lt
+    | GT _ => Gt
+  end.
+
+ Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+ Proof.
+  intros; unfold compare; destruct O.compare; auto.
+ Qed.
+
+End Update_OT.
+
+(** ** From OrderedType to OrderedTypeOrig. *)
+
+Module Backport_OT (O:OrderedType) <: OrderedTypeOrig.
+
+ Include Backport_DT O. (* Provides : t eq eq_refl eq_sym eq_trans eq_dec *)
+
+ Definition lt := O.lt.
+
+ Lemma lt_not_eq : forall x y, lt x y -> ~eq x y.
+ Proof.
+  intros x y L E; rewrite E in L. apply (StrictOrder_Irreflexive y); auto.
+ Qed.
+
+ Lemma lt_trans : Transitive lt.
+ Proof. apply O.lt_strorder. Qed.
+
+ Definition compare : forall x y, Compare lt eq x y.
+ Proof.
+  intros. assert (H:=O.compare_spec x y).
+  destruct (O.compare x y); [apply EQ|apply LT|apply GT];
+   inversion H; auto.
+ Defined.
+
+End Backport_OT.
+
+
+(** ** From OrderedTypeAlt to OrderedType. *)
+
+Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
+
+ Definition t := t.
+
+ Definition eq x y := (x?=y) = Eq.
+ Definition lt x y := (x?=y) = Lt.
+
+ Instance eq_equiv : Equivalence eq.
+ Proof.
+  split; red.
+  (* refl *)
+  unfold eq; intros x.
+  assert (H:=compare_sym x x).
+  destruct (x ?= x); simpl in *; auto; discriminate.
+  (* sym *)
+  unfold eq; intros x y H.
+  rewrite compare_sym, H; simpl; auto.
+  (* trans *)
+  apply compare_trans.
+ Qed.
+
+ Instance lt_strorder : StrictOrder lt.
+ Proof.
+  split; repeat red; unfold lt; try apply compare_trans.
+  intros x H.
+  assert (eq x x) by reflexivity.
+  unfold eq in *; congruence.
+ Qed.
+
+ Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.
+ Proof.
+  unfold lt, eq; intros x y z Hxy Hyz.
+  destruct (compare x z) as [ ]_eqn:Hxz; auto.
+  rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz.
+  rewrite (compare_trans Hxz Hyz) in Hxy; discriminate.
+  rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy.
+  rewrite (compare_trans Hxy Hxz) in Hyz; discriminate.
+ Qed.
+
+ Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z.
+ Proof.
+  unfold lt, eq; intros x y z Hxy Hyz.
+  destruct (compare x z) as [ ]_eqn:Hxz; auto.
+  rewrite compare_sym, CompOpp_iff in Hxy. simpl in Hxy.
+  rewrite (compare_trans Hxy Hxz) in Hyz; discriminate.
+  rewrite compare_sym, CompOpp_iff in Hyz. simpl in Hyz.
+  rewrite (compare_trans Hxz Hyz) in Hxy; discriminate.
+ Qed.
+
+ Instance lt_compat : Proper (eq==>eq==>iff) lt.
+ Proof.
+  apply proper_sym_impl_iff_2; auto with *.
+  repeat red; intros.
+  eapply lt_eq; eauto. eapply eq_lt; eauto. symmetry; auto.
+ Qed.
+
+ Definition compare := O.compare.
+
+ Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+ Proof.
+  unfold eq, lt, compare; intros.
+  destruct (O.compare x y) as [ ]_eqn:H; auto.
+  apply CompGt.
+  rewrite compare_sym, H; auto.
+ Qed.
+
+ 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 OT_from_Alt.
+
+(** From the original presentation to this alternative one. *)
+
+Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt.
+
+ Definition t := t.
+ Definition compare := compare.
+
+ Infix "?=" := compare (at level 70, no associativity).
+
+ Lemma compare_sym :
+   forall x y, (y?=x) = CompOpp (x?=y).
+ Proof.
+ intros x y; unfold compare.
+ destruct (compare_spec x y) as [U|U|U];
+  destruct (compare_spec y x) as [V|V|V]; auto.
+ rewrite U in V. elim (StrictOrder_Irreflexive y); auto.
+ rewrite U in V. elim (StrictOrder_Irreflexive y); auto.
+ rewrite V in U. elim (StrictOrder_Irreflexive x); auto.
+ rewrite V in U. elim (StrictOrder_Irreflexive x); auto.
+ rewrite V in U. elim (StrictOrder_Irreflexive x); auto.
+ rewrite V in U. elim (StrictOrder_Irreflexive y); auto.
+ Qed.
+
+ Lemma compare_Eq : forall x y, compare x y = Eq <-> eq x y.
+ Proof.
+ unfold compare.
+ intros x y; destruct (compare_spec x y); intuition;
+  try discriminate.
+ rewrite H0 in H. elim (StrictOrder_Irreflexive y); auto.
+ rewrite H0 in H. elim (StrictOrder_Irreflexive y); auto.
+ Qed.
+
+ Lemma compare_Lt : forall x y, compare x y = Lt <-> lt x y.
+ Proof.
+ unfold compare.
+ intros x y; destruct (compare_spec x y); intuition;
+  try discriminate.
+ rewrite H in H0. elim (StrictOrder_Irreflexive y); auto.
+ rewrite H in H0. elim (StrictOrder_Irreflexive x); auto.
+ Qed.
+
+ Lemma compare_Gt : forall x y, compare x y = Gt <-> lt y x.
+ Proof.
+ intros x y. rewrite compare_sym, CompOpp_iff. apply compare_Lt.
+ Qed.
+
+ Lemma compare_trans :
+   forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
+ Proof.
+ intros c x y z.
+ destruct c; unfold compare;
+  rewrite ?compare_Eq, ?compare_Lt, ?compare_Gt;
+  transitivity y; auto.
+ Qed.
+
+End OT_to_Alt.
diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v
new file mode 100644
index 0000000000..56f1d5dedd
--- /dev/null
+++ b/theories/Structures/OrdersEx.v
@@ -0,0 +1,88 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(* Finite sets library.
+ * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
+ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id$ *)
+
+Require Import Orders NatOrderedType POrderedType NOrderedType
+ ZOrderedType RelationPairs EqualitiesFacts.
+
+(** * Examples of Ordered Type structures. *)
+
+
+(** Ordered Type for [nat], [Positive], [N], [Z] with the usual order. *)
+
+Module Nat_as_OT := NatOrderedType.Nat_as_OT.
+Module Positive_as_OT := POrderedType.Positive_as_OT.
+Module N_as_OT := NOrderedType.N_as_OT.
+Module Z_as_OT := ZOrderedType.Z_as_OT.
+
+(** 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 := 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 ordered types, we can build a new OrderedType
+   over their cartesian product, using the lexicographic order. *)
+
+Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
+ Include PairDecidableType O1 O2.
+
+ Definition lt :=
+   (relation_disjunction (O1.lt @@1) (O1.eq * O2.lt))%signature.
+
+ Instance lt_strorder : StrictOrder lt.
+ Proof.
+ split.
+ (* irreflexive *)
+ intros (x1,x2); compute. destruct 1.
+ apply (StrictOrder_Irreflexive x1); auto.
+ apply (StrictOrder_Irreflexive x2); intuition.
+ (* transitive *)
+ intros (x1,x2) (y1,y2) (z1,z2). compute. intuition.
+ left; etransitivity; eauto.
+ left. setoid_replace z1 with y1; auto with relations.
+ left; setoid_replace x1 with y1; auto with relations.
+ right; split; etransitivity; eauto.
+ Qed.
+
+ Instance lt_compat : Proper (eq==>eq==>iff) lt.
+ Proof.
+ compute.
+ intros (x1,x2) (x1',x2') (X1,X2) (y1,y2) (y1',y2') (Y1,Y2).
+ rewrite X1,X2,Y1,Y2; intuition.
+ Qed.
+
+ Definition compare x y :=
+  match O1.compare (fst x) (fst y) with
+   | Eq => O2.compare (snd x) (snd y)
+   | Lt => Lt
+   | Gt => Gt
+  end.
+
+ Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+ Proof.
+ intros (x1,x2) (y1,y2); unfold compare; simpl.
+ destruct (O1.compare_spec x1 y1); try (constructor; compute; auto).
+ destruct (O2.compare_spec x2 y2); constructor; compute; auto with relations.
+ Qed.
+
+End PairOrderedType.
+
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
new file mode 100644
index 0000000000..a318ecb858
--- /dev/null
+++ b/theories/Structures/OrdersFacts.v
@@ -0,0 +1,234 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+Require Import Basics OrdersTac.
+Require Export Orders.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Properties of [OrderedTypeFull] *)
+
+Module OrderedTypeFullFacts (Import O:OrderedTypeFull').
+
+ Module OrderTac := OTF_to_OrderTac O.
+ Ltac order := OrderTac.order.
+ Ltac iorder := intuition order.
+
+ Instance le_compat : Proper (eq==>eq==>iff) le.
+ Proof. repeat red; iorder. Qed.
+
+ Instance le_preorder : PreOrder le.
+ Proof. split; red; order. Qed.
+
+ Instance le_order : PartialOrder eq le.
+ Proof. compute; iorder. Qed.
+
+ Instance le_antisym : Antisymmetric _ eq le.
+ Proof. apply partial_order_antisym; auto with *. Qed.
+
+ Lemma le_not_gt_iff : forall x y, x<=y <-> ~y<x.
+ Proof. iorder. Qed.
+
+ Lemma lt_not_ge_iff : forall x y, x<y <-> ~y<=x.
+ Proof. iorder. Qed.
+
+ Lemma le_or_gt : forall x y, x<=y \/ y<x.
+ Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed.
+
+ Lemma lt_or_ge : forall x y, x<y \/ y<=x.
+ Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); iorder. Qed.
+
+ Lemma eq_is_le_ge : forall x y, x==y <-> x<=y /\ y<=x.
+ Proof. iorder. Qed.
+
+End OrderedTypeFullFacts.
+
+
+(** * Properties of [OrderedType] *)
+
+Module OrderedTypeFacts (Import O: OrderedType').
+
+  Module OrderTac := OT_to_OrderTac O.
+  Ltac order := OrderTac.order.
+
+  Notation "x <= y" := (~lt y x) : order.
+  Infix "?=" := compare (at level 70, no associativity) : order.
+
+  Local Open Scope order.
+
+  Tactic Notation "elim_compare" constr(x) constr(y) :=
+   destruct (compare_spec x y).
+
+  Tactic Notation "elim_compare" constr(x) constr(y) "as" ident(h) :=
+   destruct (compare_spec x y) as [h|h|h].
+
+  (** The following lemmas are either re-phrasing of [eq_equiv] and
+      [lt_strorder] or immediately provable by [order]. Interest:
+      compatibility, test of order, etc *)
+
+  Definition eq_refl (x:t) : x==x := Equivalence_Reflexive x.
+
+  Definition eq_sym (x y:t) : x==y -> y==x := Equivalence_Symmetric x y.
+
+  Definition eq_trans (x y z:t) : x==y -> y==z -> x==z :=
+   Equivalence_Transitive x y z.
+
+  Definition lt_trans (x y z:t) : x<y -> y<z -> x<z :=
+   StrictOrder_Transitive x y z.
+
+  Definition lt_irrefl (x:t) : ~x<x := StrictOrder_Irreflexive x.
+
+  (** Some more about [compare] *)
+
+  Lemma compare_eq_iff : forall x y, (x ?= y) = Eq <-> x==y.
+  Proof.
+   intros; elim_compare x y; intuition; try discriminate; order.
+  Qed.
+
+  Lemma compare_lt_iff : forall x y, (x ?= y) = Lt <-> x<y.
+  Proof.
+   intros; elim_compare x y; intuition; try discriminate; order.
+  Qed.
+
+  Lemma compare_gt_iff : forall x y, (x ?= y) = Gt <-> y<x.
+  Proof.
+   intros; elim_compare x y; intuition; try discriminate; order.
+  Qed.
+
+  Lemma compare_ge_iff : forall x y, (x ?= y) <> Lt <-> y<=x.
+  Proof.
+   intros; rewrite compare_lt_iff; intuition.
+  Qed.
+
+  Lemma compare_le_iff : forall x y, (x ?= y) <> Gt <-> x<=y.
+  Proof.
+   intros; rewrite compare_gt_iff; intuition.
+  Qed.
+
+  Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.
+
+  Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare.
+  Proof.
+  intros x x' Hxx' y y' Hyy'.
+  elim_compare x' y'; autorewrite with order; order.
+  Qed.
+
+  Lemma compare_refl : forall x, (x ?= x) = Eq.
+  Proof.
+   intros; elim_compare x x; auto; order.
+  Qed.
+
+  Lemma compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y).
+  Proof.
+   intros; elim_compare x y; simpl; autorewrite with order; order.
+  Qed.
+
+  (** For compatibility reasons *)
+  Definition eq_dec := eq_dec.
+
+  Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}.
+  Proof.
+   intros; assert (H:=compare_spec x y); destruct (compare x y);
+    [ right | left | right ]; inversion_clear H; order.
+  Defined.
+
+  Definition eqb x y : bool := if eq_dec x y then true else false.
+
+  Lemma if_eq_dec : forall x y (B:Type)(b b':B),
+    (if eq_dec x y then b else b') =
+    (match compare x y with Eq => b | _ => b' end).
+  Proof.
+  intros; destruct eq_dec; elim_compare x y; auto; order.
+  Qed.
+
+  Lemma eqb_alt :
+    forall x y, eqb x y = match compare x y with Eq => true | _ => false end.
+  Proof.
+  unfold eqb; intros; apply if_eq_dec.
+  Qed.
+
+  Instance eqb_compat : Proper (eq==>eq==>Logic.eq) eqb.
+  Proof.
+  intros x x' Hxx' y y' Hyy'.
+  rewrite 2 eqb_alt, Hxx', Hyy'; auto.
+  Qed.
+
+End OrderedTypeFacts.
+
+
+
+
+
+
+(** * Tests of the order tactic
+
+    Is it at least capable of proving some basic properties ? *)
+
+Module OrderedTypeTest (Import O:OrderedType').
+  Module Import MO := OrderedTypeFacts O.
+  Local Open Scope order.
+  Lemma lt_not_eq x y : x<y -> ~x==y.  Proof. order. Qed.
+  Lemma lt_eq x y z : x<y -> y==z -> x<z. Proof. order. Qed.
+  Lemma eq_lt x y z : x==y -> y<z -> x<z. Proof. order. Qed.
+  Lemma le_eq x y z : x<=y -> y==z -> x<=z. Proof. order. Qed.
+  Lemma eq_le x y z : x==y -> y<=z -> x<=z. Proof. order. Qed.
+  Lemma neq_eq x y z : ~x==y -> y==z -> ~x==z. Proof. order. Qed.
+  Lemma eq_neq x y z : x==y -> ~y==z -> ~x==z. Proof. order. Qed.
+  Lemma le_lt_trans x y z : x<=y -> y<z -> x<z. Proof. order. Qed.
+  Lemma lt_le_trans x y z : x<y -> y<=z -> x<z. Proof. order. Qed.
+  Lemma le_trans x y z : x<=y -> y<=z -> x<=z. Proof. order. Qed.
+  Lemma le_antisym x y : x<=y -> y<=x -> x==y. Proof. order. Qed.
+  Lemma le_neq x y : x<=y -> ~x==y -> x<y. Proof. order. Qed.
+  Lemma neq_sym x y : ~x==y -> ~y==x. Proof. order. Qed.
+  Lemma lt_le x y : x<y -> x<=y. Proof. order. Qed.
+  Lemma gt_not_eq x y : y<x -> ~x==y. Proof. order. Qed.
+  Lemma eq_not_lt x y : x==y -> ~x<y. Proof. order. Qed.
+  Lemma eq_not_gt x y : x==y -> ~ y<x. Proof. order. Qed.
+  Lemma lt_not_gt x y : x<y -> ~ y<x. Proof. order. Qed.
+  Lemma eq_is_nlt_ngt x y : x==y <-> ~x<y /\ ~y<x.
+  Proof. intuition; order. Qed.
+End OrderedTypeTest.
+
+
+
+(** * Reversed OrderedTypeFull.
+
+   we can switch the orientation of the order. This is used for
+   example when deriving properties of [min] out of the ones of [max]
+   (see [GenericMinMax]).
+*)
+
+Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull.
+
+Definition t := O.t.
+Definition eq := O.eq.
+Instance eq_equiv : Equivalence eq.
+Definition eq_dec := O.eq_dec.
+
+Definition lt := flip O.lt.
+Definition le := flip O.le.
+
+Instance lt_strorder: StrictOrder lt.
+Proof. unfold lt; auto with *. Qed.
+Instance lt_compat : Proper (eq==>eq==>iff) lt.
+Proof. unfold lt; auto with *. Qed.
+
+Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
+Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed.
+
+Definition compare := flip O.compare.
+
+Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+Proof.
+intros; unfold compare, eq, lt, flip.
+destruct (O.compare_spec y x); auto with relations.
+Qed.
+
+End OrderedTypeRev.
+
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
new file mode 100644
index 0000000000..2ed0702688
--- /dev/null
+++ b/theories/Structures/OrdersLists.v
@@ -0,0 +1,256 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+Require Export RelationPairs SetoidList Orders.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Specialization of results about lists modulo. *)
+
+Module OrderedTypeLists (Import O:OrderedType).
+
+Section ForNotations.
+
+Notation In:=(InA eq).
+Notation Inf:=(lelistA lt).
+Notation Sort:=(sort lt).
+Notation NoDup:=(NoDupA eq).
+
+Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
+Proof. intros. rewrite <- H; auto. Qed.
+
+Lemma ListIn_In : forall l x, List.In x l -> In x l.
+Proof. exact (In_InA eq_equiv). Qed.
+
+Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l.
+Proof. exact (InfA_ltA lt_strorder). Qed.
+
+Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l.
+Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed.
+
+Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x.
+Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed.
+
+Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> lt x y) -> Inf x l.
+Proof. exact (@In_InfA t lt). Qed.
+
+Lemma In_Inf : forall l x, (forall y, In y l -> lt x y) -> Inf x l.
+Proof. exact (InA_InfA eq_equiv (ltA:=lt)). Qed.
+
+Lemma Inf_alt :
+ forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)).
+Proof. exact (InfA_alt eq_equiv lt_strorder lt_compat). Qed.
+
+Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
+Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat) . Qed.
+
+End ForNotations.
+
+Hint Resolve ListIn_In Sort_NoDup Inf_lt.
+Hint Immediate In_eq Inf_lt.
+
+End OrderedTypeLists.
+
+
+
+
+
+(** * Results about keys and data as manipulated in FMaps. *)
+
+
+Module KeyOrderedType(Import O:OrderedType).
+ Module Import MO:=OrderedTypeLists(O).
+
+ Section Elt.
+ Variable elt : Type.
+ Notation key:=t.
+
+  Local Open Scope signature_scope.
+
+  Definition eqk : relation (key*elt) := eq @@1.
+  Definition eqke : relation (key*elt) := eq * Logic.eq.
+  Definition ltk : relation (key*elt) := lt @@1.
+
+  Hint Unfold eqk eqke ltk.
+
+  (* eqke is stricter than eqk *)
+
+  Global Instance eqke_eqk : subrelation eqke eqk.
+  Proof. firstorder. Qed.
+
+  (* eqk, eqke are equalities, ltk is a strict order *)
+
+  Global Instance eqk_equiv : Equivalence eqk.
+
+  Global Instance eqke_equiv : Equivalence eqke.
+
+  Global Instance ltk_strorder : StrictOrder ltk.
+
+  Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
+  Proof. unfold eqk, ltk; auto with *. Qed.
+
+  (* Additionnal facts *)
+
+  Global Instance pair_compat : Proper (eq==>Logic.eq==>eqke) (@pair key elt).
+  Proof. apply pair_compat. Qed.
+
+  Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'.
+  Proof.
+  intros e e' LT EQ; rewrite EQ in LT.
+  elim (StrictOrder_Irreflexive _ LT).
+  Qed.
+
+  Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'.
+  Proof.
+  intros e e' LT EQ; rewrite EQ in LT.
+  elim (StrictOrder_Irreflexive _ LT).
+  Qed.
+
+  Lemma InA_eqke_eqk :
+     forall x m, InA eqke x m -> InA eqk x m.
+  Proof.
+    unfold eqke, RelProd; induction 1; firstorder.
+  Qed.
+  Hint Resolve InA_eqke_eqk.
+
+  Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
+  Definition In k m := exists e:elt, MapsTo k e m.
+  Notation Sort := (sort ltk).
+  Notation Inf := (lelistA ltk).
+
+  Hint Unfold MapsTo In.
+
+  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
+
+  Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
+  Proof.
+  firstorder.
+  exists x; auto.
+  induction H.
+  destruct y; compute in H.
+  exists e; left; auto.
+  destruct IHInA as [e H0].
+  exists e; auto.
+  Qed.
+
+  Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l.
+  Proof.
+  unfold In, MapsTo.
+  setoid_rewrite Exists_exists; setoid_rewrite InA_alt.
+  firstorder.
+  exists (snd x), x; auto.
+  Qed.
+
+  Lemma In_nil : forall k, In k nil <-> False.
+  Proof.
+  intros; rewrite In_alt2; apply Exists_nil.
+  Qed.
+
+  Lemma In_cons : forall k p l,
+   In k (p::l) <-> eq k (fst p) \/ In k l.
+  Proof.
+  intros; rewrite !In_alt2, Exists_cons; intuition.
+  Qed.
+
+  Global Instance MapsTo_compat :
+   Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo.
+  Proof.
+  intros x x' Hx e e' He l l' Hl. unfold MapsTo.
+  rewrite Hx, He, Hl; intuition.
+  Qed.
+
+  Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In.
+  Proof.
+  intros x x' Hx l l' Hl. rewrite !In_alt.
+  setoid_rewrite Hl. setoid_rewrite Hx. intuition.
+  Qed.
+
+  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
+  Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed.
+
+  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
+  Proof. intros l x y EQ. rewrite <- EQ; auto. Qed.
+
+  Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.
+  Proof. intros l x x' H. rewrite H; auto. Qed.
+
+  Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
+  Proof. apply InfA_ltA; auto with *. Qed.
+
+  Hint Immediate Inf_eq.
+  Hint Resolve Inf_lt.
+
+  Lemma Sort_Inf_In :
+      forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p.
+  Proof. apply SortA_InfA_InA; auto with *. Qed.
+
+  Lemma Sort_Inf_NotIn :
+      forall l k e, Sort l -> Inf (k,e) l ->  ~In k l.
+  Proof.
+    intros; red; intros.
+    destruct H1 as [e' H2].
+    elim (@ltk_not_eqk (k,e) (k,e')).
+    eapply Sort_Inf_In; eauto.
+    repeat red; reflexivity.
+  Qed.
+
+  Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l.
+  Proof. apply SortA_NoDupA; auto with *. Qed.
+
+  Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'.
+  Proof.
+   intros; invlist sort; eapply Sort_Inf_In; eauto.
+  Qed.
+
+  Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) ->
+      ltk e e' \/ eqk e e'.
+  Proof.
+    intros; invlist InA; auto with relations.
+    left; apply Sort_In_cons_1 with l; auto with relations.
+  Qed.
+
+  Lemma Sort_In_cons_3 :
+    forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k.
+  Proof.
+    intros; invlist sort; red; intros.
+    eapply Sort_Inf_NotIn; eauto using In_eq.
+  Qed.
+
+  Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
+  Proof.
+    intros; invlist In; invlist MapsTo. compute in * |- ; intuition.
+    right; exists x; auto.
+  Qed.
+
+  Lemma In_inv_2 : forall k k' e e' l,
+      InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
+  Proof.
+   intros; invlist InA; intuition.
+  Qed.
+
+  Lemma In_inv_3 : forall x x' l,
+      InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
+  Proof.
+   intros; invlist InA; compute in * |- ; intuition.
+  Qed.
+
+ End Elt.
+
+ Hint Unfold eqk eqke ltk.
+ Hint Extern 2 (eqke ?a ?b) => split.
+ Hint Resolve ltk_not_eqk ltk_not_eqke.
+ Hint Resolve InA_eqke_eqk.
+ Hint Unfold MapsTo In.
+ Hint Immediate Inf_eq.
+ Hint Resolve Inf_lt.
+ Hint Resolve Sort_Inf_NotIn.
+ Hint Resolve In_inv_2 In_inv_3.
+
+End KeyOrderedType.
+
diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v
new file mode 100644
index 0000000000..80be890265
--- /dev/null
+++ b/theories/Structures/OrdersTac.v
@@ -0,0 +1,323 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+Require Import Setoid Morphisms Basics Equalities Orders.
+Set Implicit Arguments.
+
+(** * The order tactic *)
+
+(** This tactic is designed to solve systems of (in)equations
+    involving [eq], [lt], [le] and [~eq] on some type. This tactic is
+    domain-agnostic; it will only use equivalence+order axioms, and
+    not analyze elements of the domain. Hypothesis or goal of the form
+    [~lt] or [~le] are initially turned into [le] and [lt], other
+    parts of the goal are ignored. This initial preparation of the
+    goal is the only moment where totality is used. In particular,
+    the core of the tactic only proceeds by saturation of transitivity
+    and similar properties, and does not perform case splitting.
+    The tactic will fail if it doesn't solve the goal. *)
+
+
+(** An abstract vision of the predicates. This allows a one-line
+    statement for interesting transitivity properties: for instance
+    [trans_ord OLE OLE = OLE] will imply later
+    [le x y -> le y z -> le x z].
+*)
+
+Inductive ord := OEQ | OLT | OLE.
+Definition trans_ord o o' :=
+ match o, o' with
+ | OEQ, _ => o'
+ | _, OEQ => o
+ | OLE, OLE => OLE
+ | _, _ => OLT
+ end.
+Local Infix "+" := trans_ord.
+
+
+(** ** The requirements of the tactic : [TotalOrder].
+
+   [TotalOrder] contains an equivalence [eq],
+   a strict order [lt] total and compatible with [eq], and
+   a larger order [le] synonym for [lt\/eq].
+
+  NB: we create here a clone of TotalOrder, but without the [Inline] Pragma.
+  This is important for having later the exact shape in Ltac matching.
+*)
+
+Module Type TotalOrder_NoInline <: TotalOrder.
+ Parameter Inline t : Type.
+ Parameters eq lt le : t -> t -> Prop.
+ Include IsEq <+ IsStrOrder <+ LeIsLtEq <+ LtIsTotal.
+End TotalOrder_NoInline.
+
+Module Type TotalOrder_NoInline' := TotalOrder_NoInline <+ EqLtLeNotation.
+
+(** We make explicit aliases to help ltac matching *)
+
+Module CloneOrder (O:TotalOrder_NoInline) <: TotalOrder.
+Definition t := O.t.
+Definition eq := O.eq.
+Definition lt := O.lt.
+Definition le := O.le.
+Definition eq_equiv := O.eq_equiv.
+Definition lt_compat := O.lt_compat.
+Definition lt_strorder := O.lt_strorder.
+Definition le_lteq := O.le_lteq.
+Definition lt_total := O.lt_total.
+End CloneOrder.
+
+
+
+(** ** Properties that will be used by the [order] tactic *)
+
+Module OrderFacts(Import O:TotalOrder_NoInline').
+
+(** Reflexivity rules *)
+
+Lemma eq_refl : forall x, x==x.
+Proof. reflexivity. Qed.
+
+Lemma le_refl : forall x, x<=x.
+Proof. intros; rewrite le_lteq; right; reflexivity. Qed.
+
+Lemma lt_irrefl : forall x, ~ x<x.
+Proof. intros; apply StrictOrder_Irreflexive. Qed.
+
+(** Symmetry rules *)
+
+Lemma eq_sym : forall x y, x==y -> y==x.
+Proof. auto with *. Qed.
+
+Lemma le_antisym : forall x y, x<=y -> y<=x -> x==y.
+Proof.
+ intros x y; rewrite 2 le_lteq. intuition.
+ elim (StrictOrder_Irreflexive x); transitivity y; auto.
+Qed.
+
+Lemma neq_sym : forall x y, ~x==y -> ~y==x.
+Proof. auto using eq_sym. Qed.
+
+(** Transitivity rules : first, a generic formulation, then instances*)
+
+Ltac subst_eqns :=
+ match goal with
+   | H : _==_ |- _ => (rewrite H || rewrite <- H); clear H; subst_eqns
+   | _ => idtac
+ end.
+
+Definition interp_ord o :=
+ match o with OEQ => O.eq | OLT => O.lt | OLE => O.le end.
+Local Notation "#" := interp_ord.
+
+Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z.
+Proof.
+destruct o, o'; simpl; intros x y z; rewrite ?le_lteq; intuition;
+ subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
+Qed.
+
+Definition eq_trans x y z : x==y -> y==z -> x==z := @trans OEQ OEQ x y z.
+Definition le_trans x y z : x<=y -> y<=z -> x<=z := @trans OLE OLE x y z.
+Definition lt_trans x y z : x<y -> y<z -> x<z := @trans OLT OLT x y z.
+Definition le_lt_trans x y z : x<=y -> y<z -> x<z := @trans OLE OLT x y z.
+Definition lt_le_trans x y z : x<y -> y<=z -> x<z := @trans OLT OLE x y z.
+Definition eq_lt x y z : x==y -> y<z -> x<z := @trans OEQ OLT x y z.
+Definition lt_eq x y z : x<y -> y==z -> x<z := @trans OLT OEQ x y z.
+Definition eq_le x y z : x==y -> y<=z -> x<=z := @trans OEQ OLE x y z.
+Definition le_eq x y z : x<=y -> y==z -> x<=z := @trans OLE OEQ x y z.
+
+Lemma eq_neq : forall x y z, x==y -> ~y==z -> ~x==z.
+Proof. eauto using eq_trans, eq_sym. Qed.
+
+Lemma neq_eq : forall x y z, ~x==y -> y==z -> ~x==z.
+Proof. eauto using eq_trans, eq_sym. Qed.
+
+(** (double) negation rules *)
+
+Lemma not_neq_eq : forall x y, ~~x==y -> x==y.
+Proof.
+intros x y H. destruct (lt_total x y) as [H'|[H'|H']]; auto;
+ destruct H; intro H; rewrite H in H'; eapply lt_irrefl; eauto.
+Qed.
+
+Lemma not_ge_lt : forall x y, ~y<=x -> x<y.
+Proof.
+intros x y H. destruct (lt_total x y); auto.
+destruct H. rewrite le_lteq. intuition.
+Qed.
+
+Lemma not_gt_le : forall x y, ~y<x -> x<=y.
+Proof.
+intros x y H. rewrite le_lteq. generalize (lt_total x y); intuition.
+Qed.
+
+Lemma le_neq_lt : forall x y, x<=y -> ~x==y -> x<y.
+Proof. auto using not_ge_lt, le_antisym. Qed.
+
+End OrderFacts.
+
+
+
+(** ** [MakeOrderTac] : The functor providing the order tactic. *)
+
+Module MakeOrderTac (Import O:TotalOrder_NoInline').
+
+Include OrderFacts O.
+
+(** order_eq : replace x by y in all (in)equations hyps thanks
+   to equality EQ (where eq has been hidden in order to avoid
+   self-rewriting), then discard EQ. *)
+
+Ltac order_rewr x eqn :=
+ (* NB: we could use the real rewrite here, but proofs would be uglier. *)
+ let rewr H t := generalize t; clear H; intro H
+ in
+ match goal with
+ | H : x == _ |- _ => rewr H (eq_trans (eq_sym eqn) H); order_rewr x eqn
+ | H : _ == x |- _ => rewr H (eq_trans H eqn); order_rewr x eqn
+ | H : ~x == _ |- _ => rewr H (eq_neq (eq_sym eqn) H); order_rewr x eqn
+ | H : ~_ == x |- _ => rewr H (neq_eq H eqn); order_rewr x eqn
+ | H : x < _ |- _ => rewr H (eq_lt (eq_sym eqn) H); order_rewr x eqn
+ | H : _ < x |- _ => rewr H (lt_eq H eqn); order_rewr x eqn
+ | H : x <= _ |- _ => rewr H (eq_le (eq_sym eqn) H); order_rewr x eqn
+ | H : _ <= x |- _ => rewr H (le_eq H eqn); order_rewr x eqn
+ | _ => clear eqn
+end.
+
+Ltac order_eq x y eqn :=
+ match x with
+ | y => clear eqn
+ | _ => change (interp_ord OEQ x y) in eqn; order_rewr x eqn
+ end.
+
+(** Goal preparation : We turn all negative hyps into positive ones
+  and try to prove False from the inverse of the current goal.
+  These steps require totality of our order. After this preparation,
+  order only deals with the context, and tries to prove False.
+  Hypotheses of the form [A -> False] are also folded in [~A]
+  for convenience (i.e. cope with the mess left by intuition). *)
+
+Ltac order_prepare :=
+ match goal with
+ | H : ?A -> False |- _ => change (~A) in H; order_prepare
+ | H : ~(?R ?x ?y) |- _ =>
+   match R with
+   | eq => fail 1 (* if already using [eq], we leave it this ways *)
+   | _ => (change (~x==y) in H ||
+           apply not_gt_le in H ||
+           apply not_ge_lt in H ||
+           clear H || fail 1); order_prepare
+   end
+ | H : ?R ?x ?y |- _ =>
+   match R with
+   | eq => fail 1
+   | lt => fail 1
+   | le => fail 1
+   | _ => (change (x==y) in H ||
+           change (x<y) in H ||
+           change (x<=y) in H ||
+           clear H || fail 1); order_prepare
+   end
+ | |- ~ _ => intro; order_prepare
+ | |- _ ?x ?x =>
+   exact (eq_refl x) || exact (le_refl x) || exfalso
+ | _ =>
+   (apply not_neq_eq; intro) ||
+   (apply not_ge_lt; intro) ||
+   (apply not_gt_le; intro) || exfalso
+ end.
+
+(** We now try to prove False from the various [< <= == !=] hypothesis *)
+
+Ltac order_loop :=
+ match goal with
+ (* First, successful situations *)
+ | H : ?x < ?x |- _ => exact (lt_irrefl H)
+ | H : ~ ?x == ?x |- _ => exact (H (eq_refl x))
+ (* Second, useless hyps *)
+ | H : ?x <= ?x |- _ => clear H; order_loop
+ (* Third, we eliminate equalities *)
+ | H : ?x == ?y |- _ => order_eq x y H; order_loop
+ (* Simultaneous le and ge is eq *)
+ | H1 : ?x <= ?y, H2 : ?y <= ?x |- _ =>
+     generalize (le_antisym H1 H2); clear H1 H2; intro; order_loop
+ (* Simultaneous le and ~eq is lt *)
+ | H1: ?x <= ?y, H2: ~ ?x == ?y |- _ =>
+     generalize (le_neq_lt H1 H2); clear H1 H2; intro; order_loop
+ | H1: ?x <= ?y, H2: ~ ?y == ?x |- _ =>
+     generalize (le_neq_lt H1 (neq_sym H2)); clear H1 H2; intro; order_loop
+ (* Transitivity of lt and le *)
+ | H1 : ?x < ?y, H2 : ?y < ?z |- _ =>
+    match goal with
+      | H : x < z |- _ => fail 1
+      | _ => generalize (lt_trans H1 H2); intro; order_loop
+    end
+ | H1 : ?x <= ?y, H2 : ?y < ?z |- _ =>
+    match goal with
+      | H : x < z |- _ => fail 1
+      | _ => generalize (le_lt_trans H1 H2); intro; order_loop
+    end
+ | H1 : ?x < ?y, H2 : ?y <= ?z |- _ =>
+    match goal with
+      | H : x < z |- _ => fail 1
+      | _ => generalize (lt_le_trans H1 H2); intro; order_loop
+    end
+ | H1 : ?x <= ?y, H2 : ?y <= ?z |- _ =>
+    match goal with
+      | H : x <= z |- _ => fail 1
+      | _ => generalize (le_trans H1 H2); intro; order_loop
+    end
+ | _ => idtac
+end.
+
+(** The complete tactic. *)
+
+Ltac order :=
+ intros; order_prepare; order_loop; fail "Order tactic unsuccessful".
+
+End MakeOrderTac.
+
+Module OTF_to_OrderTac (OTF:OrderedTypeFull).
+ Module TO := OTF_to_TotalOrder OTF.
+ Module TO' := CloneOrder TO.
+ Include MakeOrderTac TO'.
+End OTF_to_OrderTac.
+
+Module OT_to_OrderTac (OT:OrderedType).
+ Module OTF := OT_to_Full OT.
+ Include OTF_to_OrderTac OTF.
+End OT_to_OrderTac.
+
+(** For example of use of this tactic, see for instance [OrderedType] *)
+
+
+Module TotalOrderRev (O:TotalOrder) <: TotalOrder.
+
+Definition t := O.t.
+Definition eq := O.eq.
+Definition lt := flip O.lt.
+Definition le := flip O.le.
+Include EqLtLeNotation.
+
+Instance eq_equiv : Equivalence eq.
+
+Instance lt_strorder: StrictOrder lt.
+Proof. unfold lt; auto with *. Qed.
+Instance lt_compat : Proper (eq==>eq==>iff) lt.
+Proof. unfold lt; auto with *. Qed.
+
+Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y.
+Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed.
+
+Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
+Proof.
+ intros x y; unfold lt, eq, flip.
+ generalize (O.lt_total x y); intuition.
+Qed.
+
+End TotalOrderRev.
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 *)
-- 
cgit v1.2.3