summaryrefslogtreecommitdiff
path: root/theories/FSets/OrderedTypeAlt.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /theories/FSets/OrderedTypeAlt.v
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/FSets/OrderedTypeAlt.v')
-rw-r--r--theories/FSets/OrderedTypeAlt.v24
1 files changed, 8 insertions, 16 deletions
diff --git a/theories/FSets/OrderedTypeAlt.v b/theories/FSets/OrderedTypeAlt.v
index 9bcfbfc7..516df0f0 100644
--- a/theories/FSets/OrderedTypeAlt.v
+++ b/theories/FSets/OrderedTypeAlt.v
@@ -11,19 +11,19 @@
* Institution: LRI, CNRS UMR 8623 - Université Paris Sud
* 91405 Orsay, France *)
-(* $Id: OrderedTypeAlt.v 8773 2006-04-29 14:31:32Z letouzey $ *)
+(* $Id: OrderedTypeAlt.v 10739 2008-04-01 14:45:20Z herbelin $ *)
Require Import OrderedType.
(** * An alternative (but equivalent) presentation for an Ordered Type inferface. *)
-(** NB: [comparison], defined in [theories/Init/datatypes.v] is [Eq|Lt|Gt]
-whereas [compare], defined in [theories/FSets/OrderedType.v] is [EQ _ | LT _ | GT _ ]
+(** NB: [comparison], defined in [Datatypes.v] is [Eq|Lt|Gt]
+whereas [compare], defined in [OrderedType.v] is [EQ _ | LT _ | GT _ ]
*)
Module Type OrderedTypeAlt.
- Parameter t : Set.
+ Parameter t : Type.
Parameter compare : t -> t -> comparison.
@@ -103,24 +103,16 @@ Module OrderedType_to_Alt (O:OrderedType) <: OrderedTypeAlt.
Lemma compare_sym :
forall x y, (y?=x) = CompOpp (x?=y).
Proof.
- intros x y.
- unfold compare.
- destruct (O.compare y x); elim_comp; simpl; auto.
+ intros x y; unfold compare.
+ destruct O.compare; elim_comp; simpl; auto.
Qed.
Lemma compare_trans :
forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
Proof.
intros c x y z.
- destruct c; unfold compare.
- destruct (O.compare x y); intros; try discriminate.
- destruct (O.compare y z); intros; try discriminate.
- elim_comp; auto.
- destruct (O.compare x y); intros; try discriminate.
- destruct (O.compare y z); intros; try discriminate.
- elim_comp; auto.
- destruct (O.compare x y); intros; try discriminate.
- destruct (O.compare y z); intros; try discriminate.
+ destruct c; unfold compare;
+ do 2 (destruct O.compare; intros; try discriminate);
elim_comp; auto.
Qed.