diff options
-rw-r--r-- | theories/FSets/DecidableType.v | 4 | ||||
-rw-r--r-- | theories/FSets/FMapList.v | 4 | ||||
-rw-r--r-- | theories/FSets/FMapWeakList.v | 4 | ||||
-rw-r--r-- | theories/FSets/OrderedType.v | 4 |
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. |