From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- theories/FSets/OrderedTypeAlt.v | 24 ++++++++---------------- 1 file changed, 8 insertions(+), 16 deletions(-) (limited to 'theories/FSets/OrderedTypeAlt.v') 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. -- cgit v1.2.3