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

5 files changed, 8 insertions, 9 deletions

diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index cb18785e6..0de28d5e8 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 4292eb938..b0caf6692 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 dc82a1450..a9ba0a823 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 f805a3c96..f0b964cf2 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 42966c7fc..558b09562 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.