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

14 files changed, 95 insertions, 118 deletions

diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
index de7a20d4c5..2c72e30b16 100644
--- a/theories/Structures/DecidableType.v
+++ b/theories/Structures/DecidableType.v
@@ -9,19 +9,21 @@
 (* $Id$ *)
 
 Require Export SetoidList.
-Require DecidableType2. (* No Import here, this is on purpose. *)
+Require Equalities.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+(** NB: This file is here only for compatibility with earlier version of
+    [FSets] and [FMap]. Please use [Structures/Equalities.v] directly now. *)
 
 (** * Types with Equalities, and nothing more (for subtyping purpose) *)
 
-Module Type EqualityType := DecidableType2.EqualityTypeOrig.
+Module Type EqualityType := Equalities.EqualityTypeOrig.
 
 (** * Types with decidable Equalities (but no ordering) *)
 
-Module Type DecidableType := DecidableType2.DecidableTypeOrig.
+Module Type DecidableType := Equalities.DecidableTypeOrig.
 
 (** * Additional notions about keys and datas used in FMap *)
 
diff --git a/theories/Structures/DecidableType2Ex.v b/theories/Structures/DecidableType2Ex.v
deleted file mode 100644
index 2ce2b56623..0000000000
--- a/theories/Structures/DecidableType2Ex.v
+++ /dev/null
@@ -1,53 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-Require Import DecidableType2 Morphisms RelationPairs.
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-(** * Examples of Decidable Type structures. *)
-
-
-(** From two decidable types, we can build a new DecidableType
-   over their cartesian product. *)
-
-Module PairDecidableType(D1 D2:DecidableType) <: DecidableType.
-
- Definition t := (D1.t * D2.t)%type.
-
- Definition eq := (D1.eq * D2.eq)%signature.
-
- Instance eq_equiv : Equivalence eq.
-
- Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
- Proof.
- intros (x1,x2) (y1,y2); unfold eq; simpl.
- destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
-  compute; intuition.
- Defined.
-
-End PairDecidableType.
-
-(** Similarly for pairs of UsualDecidableType *)
-
-Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
- Definition t := (D1.t * D2.t)%type.
- Definition eq := @eq t.
- Program Instance eq_equiv : Equivalence eq.
- Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
- Proof.
- intros (x1,x2) (y1,y2);
- destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
- unfold eq, D1.eq, D2.eq in *; simpl;
- (left; f_equal; auto; fail) ||
- (right; intro H; injection H; auto).
- Defined.
-
-End PairUsualDecidableType.
diff --git a/theories/Structures/DecidableTypeEx.v b/theories/Structures/DecidableTypeEx.v
index 022102f70d..4407ead416 100644
--- a/theories/Structures/DecidableTypeEx.v
+++ b/theories/Structures/DecidableTypeEx.v
@@ -12,19 +12,15 @@ Require Import DecidableType OrderedType OrderedTypeEx.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+(** NB: This file is here only for compatibility with earlier version of
+    [FSets] and [FMap]. Please use [Structures/Equalities.v] directly now. *)
+
 (** * Examples of Decidable Type structures. *)
 
 (** A particular case of [DecidableType] where
     the equality is the usual one of Coq. *)
 
-Module Type UsualDecidableType.
- Parameter Inline t : Type.
- Definition eq := @eq t.
- Definition eq_refl := @refl_equal t.
- Definition eq_sym := @sym_eq t.
- Definition eq_trans := @trans_eq t.
- Parameter eq_dec : forall x y, { eq x y }+{~eq x y }.
-End UsualDecidableType.
+Module Type UsualDecidableType := Equalities.UsualDecidableTypeOrig.
 
 (** a [UsualDecidableType] is in particular an [DecidableType]. *)
 
@@ -32,19 +28,10 @@ Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U.
 
 (** an shortcut for easily building a UsualDecidableType *)
 
-Module Type MiniDecidableType.
- Parameter Inline t : Type.
- Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }.
-End MiniDecidableType.
+Module Type MiniDecidableType := Equalities.MiniDecidableType.
 
-Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType.
- Definition t:=M.t.
- Definition eq := @eq t.
- Definition eq_refl := @refl_equal t.
- Definition eq_sym := @sym_eq t.
- Definition eq_trans := @trans_eq t.
- Definition eq_dec := M.eq_dec.
-End Make_UDT.
+Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType
+ := Equalities.Make_UDT M.
 
 (** An OrderedType can now directly be seen as a DecidableType *)
 
diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/Equalities.v
index 2679d25b01..76f539764a 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/Equalities.v
@@ -168,47 +168,49 @@ Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType
    A particular case of [DecidableType] where the equality is
    the usual one of Coq. *)
 
-Module Type UsualEq <: Eq.
- Parameter Inline t : Type.
- Definition eq := @eq t.
-End UsualEq.
+Module Type HasUsualEq (Import T:Typ) <: HasEq T.
+ Definition eq := @Logic.eq t.
+End HasUsualEq.
 
-Module UsualIsEq (E:UsualEq) <: IsEq E.
+Module Type UsualEq <: Eq := Typ <+ HasUsualEq.
+
+Module Type UsualIsEq (E:UsualEq) <: IsEq E.
  Program Instance eq_equiv : Equivalence E.eq.
 End UsualIsEq.
 
-Module UsualIsEqOrig (E:UsualEq) <: IsEqOrig E.
- Definition eq_refl := @eq_refl E.t.
- Definition eq_sym := @eq_sym E.t.
- Definition eq_trans := @eq_trans E.t.
+Module Type UsualIsEqOrig (E:UsualEq) <: IsEqOrig E.
+ Definition eq_refl := @Logic.eq_refl E.t.
+ Definition eq_sym := @Logic.eq_sym E.t.
+ Definition eq_trans := @Logic.eq_trans E.t.
 End UsualIsEqOrig.
 
 Module Type UsualEqualityType <: EqualityType
- := UsualEq <+ IsEq.
+ := UsualEq <+ UsualIsEq.
 
 Module Type UsualDecidableType <: DecidableType
- := UsualEq <+ IsEq <+ HasEqDec.
+ := UsualEq <+ UsualIsEq <+ HasEqDec.
+
+Module Type UsualDecidableTypeOrig <: DecidableTypeOrig
+ := UsualEq <+ UsualIsEqOrig <+ HasEqDec.
 
 Module Type UsualDecidableTypeBoth <: DecidableTypeBoth
- := UsualEq <+ IsEq <+ IsEqOrig <+ HasEqDec.
+ := UsualEq <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqDec.
 
 Module Type UsualBoolEq := UsualEq <+ HasEqBool.
 
 Module Type UsualDecidableTypeFull <: DecidableTypeFull
- := UsualEq <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
+ := UsualEq <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqDec <+ HasEqBool.
 
 
 (** Some shortcuts for easily building a [UsualDecidableType] *)
 
 Module Type MiniDecidableType.
- Parameter t : Type.
+ Include Typ.
  Parameter eq_dec : forall x y : t, {x=y}+{~x=y}.
 End MiniDecidableType.
 
-Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth.
- Definition eq := @Logic.eq M.t.
- Include M <+ UsualIsEq <+ UsualIsEqOrig.
-End Make_UDT.
+Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth
+ := M <+ HasUsualEq <+ UsualIsEq <+ UsualIsEqOrig.
 
 Module Make_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull
  := M <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqBool2Dec.
diff --git a/theories/Structures/DecidableType2Facts.v b/theories/Structures/EqualitiesFacts.v
index 07a3b8f838..d9b1d76fdf 100644
--- a/theories/Structures/DecidableType2Facts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Import DecidableType2 Bool SetoidList RelationPairs.
+Require Import Equalities Bool SetoidList RelationPairs.
 
 (** In a BooleanEqualityType, [eqb] is compatible with [eq] *)
 
@@ -145,4 +145,41 @@ Module KeyDecidableType(Import D:DecidableType).
 End KeyDecidableType.
 
 
+(** * PairDecidableType 
+   
+   From two decidable types, we can build a new DecidableType
+   over their cartesian product. *)
 
+Module PairDecidableType(D1 D2:DecidableType) <: DecidableType.
+
+ Definition t := (D1.t * D2.t)%type.
+
+ Definition eq := (D1.eq * D2.eq)%signature.
+
+ Instance eq_equiv : Equivalence eq.
+
+ Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
+ Proof.
+ intros (x1,x2) (y1,y2); unfold eq; simpl.
+ destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
+  compute; intuition.
+ Defined.
+
+End PairDecidableType.
+
+(** Similarly for pairs of UsualDecidableType *)
+
+Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
+ Definition t := (D1.t * D2.t)%type.
+ Definition eq := @eq t.
+ Program Instance eq_equiv : Equivalence eq.
+ Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
+ Proof.
+ intros (x1,x2) (y1,y2);
+ destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2);
+ unfold eq, D1.eq, D2.eq in *; simpl;
+ (left; f_equal; auto; fail) ||
+ (right; intro H; injection H; auto).
+ Defined.
+
+End PairUsualDecidableType.
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index f45e43b445..232989fad0 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Import OrderTac OrderedType2 OrderedType2Facts Setoid Morphisms Basics.
+Require Import Orders OrdersTac OrdersFacts Setoid Morphisms Basics.
 
 (** * A Generic construction of min and max *)
 
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index 1f3e50dc3f..7d56d96665 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -8,10 +8,13 @@
 
 (* $Id$ *)
 
-Require Export SetoidList Morphisms OrderTac.
+Require Export SetoidList Morphisms OrdersTac.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+(** NB: This file is here only for compatibility with earlier version of
+     [FSets] and [FMap]. Please use [Structures/Orders.v] directly now. *)
+
 (** * Ordered types *)
 
 Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type :=
@@ -103,7 +106,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
   Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x.
   Proof. intros; destruct (compare x y); auto. Qed.
 
-  Module OrderElts <: OrderedType2.TotalOrder.
+  Module OrderElts <: Orders.TotalOrder.
   Definition t := t.
   Definition eq := eq.
   Definition lt := lt.
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/Orders.v
index 766b0faf05..c71be0a6ee 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/Orders.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Require Export Relations Morphisms Setoid DecidableType2.
+Require Export Relations Morphisms Setoid Equalities.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/theories/Structures/OrderedType2Alt.v b/theories/Structures/OrdersAlt.v
index b036b50e5b..261e75e1c5 100644
--- a/theories/Structures/OrderedType2Alt.v
+++ b/theories/Structures/OrdersAlt.v
@@ -13,7 +13,7 @@
 
 (* $Id$ *)
 
-Require Import OrderedType OrderedType2.
+Require Import OrderedType Orders.
 Set Implicit Arguments.
 
 (** * Some alternative (but equivalent) presentations for an Ordered Type
diff --git a/theories/Structures/OrderedType2Ex.v b/theories/Structures/OrdersEx.v
index 1e45a3fbfb..56f1d5dedd 100644
--- a/theories/Structures/OrderedType2Ex.v
+++ b/theories/Structures/OrdersEx.v
@@ -13,8 +13,8 @@
 
 (* $Id$ *)
 
-Require Import OrderedType2 NatOrderedType POrderedType NOrderedType
- ZOrderedType DecidableType2Ex RelationPairs.
+Require Import Orders NatOrderedType POrderedType NOrderedType
+ ZOrderedType RelationPairs EqualitiesFacts.
 
 (** * Examples of Ordered Type structures. *)
 
diff --git a/theories/Structures/OrderedType2Facts.v b/theories/Structures/OrdersFacts.v
index b5dc0c92fc..a318ecb858 100644
--- a/theories/Structures/OrderedType2Facts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -6,8 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Import Basics OrderTac.
-Require Export OrderedType2.
+Require Import Basics OrdersTac.
+Require Export Orders.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Structures/OrderedType2Lists.v b/theories/Structures/OrdersLists.v
index 79690fb024..2ed0702688 100644
--- a/theories/Structures/OrderedType2Lists.v
+++ b/theories/Structures/OrdersLists.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Export RelationPairs SetoidList OrderedType2.
+Require Export RelationPairs SetoidList Orders.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrdersTac.v
index 2465dc539e..80be890265 100644
--- a/theories/Structures/OrderTac.v
+++ b/theories/Structures/OrdersTac.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Import Setoid Morphisms Basics DecidableType2 OrderedType2.
+Require Import Setoid Morphisms Basics Equalities Orders.
 Set Implicit Arguments.
 
 (** * The order tactic *)
diff --git a/theories/Structures/vo.itarget b/theories/Structures/vo.itarget
index 6500dcd89a..674e9fba9d 100644
--- a/theories/Structures/vo.itarget
+++ b/theories/Structures/vo.itarget
@@ -1,15 +1,14 @@
+Equalities.vo
+EqualitiesFacts.vo
+Orders.vo
+OrdersEx.vo
+OrdersFacts.vo
+OrdersLists.vo
+OrdersTac.vo
+OrdersAlt.vo
+GenericMinMax.vo
+DecidableType.vo
+DecidableTypeEx.vo
 OrderedTypeAlt.vo
 OrderedTypeEx.vo
 OrderedType.vo
-DecidableType.vo
-DecidableTypeEx.vo
-OrderedType2Alt.vo
-OrderedType2Ex.vo
-OrderedType2.vo
-OrderedType2Facts.vo
-OrderedType2Lists.vo
-DecidableType2.vo
-DecidableType2Ex.vo
-DecidableType2Facts.vo
-OrderTac.vo
-GenericMinMax.vo