meilleur nommage pour PairOrderedType

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

4 files changed, 8 insertions, 8 deletions

diff --git a/theories/FSets/DecidableType.v b/theories/FSets/DecidableType.v
index 1484ce8e3..4e34bbc0d 100644
--- a/theories/FSets/DecidableType.v
+++ b/theories/FSets/DecidableType.v
@@ -32,7 +32,7 @@ Module Type DecidableType.
 End DecidableType. 
 
 
-Module PairDecidableType(D:DecidableType).
+Module KeyDecidableType(D:DecidableType).
  Import D.
 
  Section Elt.
@@ -148,4 +148,4 @@ Module PairDecidableType(D:DecidableType).
  Hint Resolve In_inv_2 In_inv_3.
 
 
-End PairDecidableType.
+End KeyDecidableType.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index ae52ce6b7..7cc5230e5 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -26,7 +26,7 @@ Module Raw (X:OrderedType).
 
 Module E := X.
 Module MX := OrderedTypeFacts X.
-Module PX := PairOrderedType X.
+Module PX := KeyOrderedType X.
 Import MX. 
 Import PX. 
 
@@ -36,7 +36,7 @@ Definition t (elt:Set) := list (X.t * elt).
 Section Elt.
 Variable elt : Set.
 
-(* Now in PairOrderedtype: 
+(* Now in KeyOrderedType: 
 Definition eqk (p p':key*elt) := X.eq (fst p) (fst p').
 Definition eqke (p p':key*elt) := 
         X.eq (fst p) (fst p') /\ (snd p) = (snd p').
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index f2a324aca..bfa97d0b2 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -24,7 +24,7 @@ Arguments Scope list [type_scope].
 
 Module Raw (X:DecidableType).
 
-Module PX := PairDecidableType X.
+Module PX := KeyDecidableType X.
 Import PX.
 
 Definition key := X.t.
@@ -34,7 +34,7 @@ Section Elt.
 
 Variable elt : Set.
 
-(* now in PairDecidableType:
+(* now in KeyDecidableType:
 Definition eqk (p p':key*elt) := X.eq (fst p) (fst p').
 Definition eqke (p p':key*elt) := 
           X.eq (fst p) (fst p') /\ (snd p) = (snd p').
diff --git a/theories/FSets/OrderedType.v b/theories/FSets/OrderedType.v
index cb31b388b..0268b38c9 100644
--- a/theories/FSets/OrderedType.v
+++ b/theories/FSets/OrderedType.v
@@ -351,7 +351,7 @@ Hint Immediate In_eq Inf_lt.
 
 End OrderedTypeFacts.
 
-Module PairOrderedType(O:OrderedType).
+Module KeyOrderedType(O:OrderedType).
  Import O.
  Module MO:=OrderedTypeFacts(O).
  Import MO.
@@ -561,6 +561,6 @@ Module PairOrderedType(O:OrderedType).
  Hint Resolve Sort_Inf_NotIn.
  Hint Resolve In_inv_2 In_inv_3.
 
-End PairOrderedType.
+End KeyOrderedType.