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

4 files changed, 8 insertions, 8 deletions

diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index e2953f333..bc6c731f6 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 4a341328e..971daa215 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 950f48a90..f83259c44 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 6bf4ae989..711cbd9a6 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.