diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-28 11:59:44 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-28 11:59:44 +0000 |
| commit | 49ef74982e3d810b9296dd62a7ba30053ceb8e63 (patch) | |
| tree | 760d7ecedd7b27969fbec03c92afc70cc3562825 /theories/FSets/FMapInterface.v | |
| parent | ea9ccff8b51832dd7c1d9400d73e859f05806273 (diff) | |
reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / OrderedType.Lt,Eq,Gt
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8667 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets/FMapInterface.v')
| -rw-r--r-- | theories/FSets/FMapInterface.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v index 32cacf4c0..36cdb9775 100644 --- a/theories/FSets/FMapInterface.v +++ b/theories/FSets/FMapInterface.v @@ -229,7 +229,7 @@ Module Type Sord. Axiom lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3. Axiom lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2. - Definition cmp e e' := match Data.compare e e' with Eq _ => true | _ => false end. + Definition cmp e e' := match Data.compare e e' with EQ _ => true | _ => false end. Parameter eq_1 : forall m m', Equal cmp m m' -> eq m m'. Parameter eq_2 : forall m m', eq m m' -> Equal cmp m m'. |