diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-29 11:57:59 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-29 11:57:59 +0000 |
| commit | c03302b1783ddd7a78902689b57787bed67c1f88 (patch) | |
| tree | 23d7a4959eb05f7d7de6f29d360d54f8fff6a64c /theories/FSets/FMapList.v | |
| parent | 91e2e89e84c0eb343198b0c887b727b35f9658cd (diff) | |
meilleur nommage pour PairOrderedType
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8772 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets/FMapList.v')
| -rw-r--r-- | theories/FSets/FMapList.v | 4 |
1 files changed, 2 insertions, 2 deletions
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'). |