From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:08:29 +0000 Subject: Fusion de la branche "traces": - Ajout de traces d'evenements d'E/S dans les semantiques - Ajout constructions switch et allocation dynamique - Initialisation des variables globales - Portage Coq 8.1 beta Debut d'integration du front-end C: - Traduction Clight -> Csharpminor dans cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Ordered.v | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'lib/Ordered.v') diff --git a/lib/Ordered.v b/lib/Ordered.v index 1747bbb9..ad47314a 100644 --- a/lib/Ordered.v +++ b/lib/Ordered.v @@ -1,7 +1,7 @@ (** Constructions of ordered types, for use with the [FSet] functors for finite sets. *) -Require Import FSet. +Require Import FSets. Require Import Coqlib. Require Import Maps. @@ -26,10 +26,10 @@ Proof Plt_ne. Lemma compare : forall x y : t, Compare lt eq x y. Proof. intros. case (plt x y); intro. - apply Lt. auto. + apply LT. auto. case (peq x y); intro. - apply Eq. auto. - apply Gt. red; unfold Plt in *. + apply EQ. auto. + apply GT. red; unfold Plt in *. assert (Zpos x <> Zpos y). congruence. omega. Qed. @@ -64,9 +64,9 @@ Qed. Lemma compare : forall x y : t, Compare lt eq x y. Proof. intros. case (OrderedPositive.compare (A.index x) (A.index y)); intro. - apply Lt. exact l. - apply Eq. red; red in e. apply A.index_inj; auto. - apply Gt. exact l. + apply LT. exact l. + apply EQ. red; red in e. apply A.index_inj; auto. + apply GT. exact l. Qed. End OrderedIndexed. @@ -144,12 +144,12 @@ Lemma compare : forall x y : t, Compare lt eq x y. Proof. intros. case (A.compare (fst x) (fst y)); intro. - apply Lt. red. left. auto. + apply LT. red. left. auto. case (B.compare (snd x) (snd y)); intro. - apply Lt. red. right. tauto. - apply Eq. red. tauto. - apply Gt. red. right. split. apply A.eq_sym. auto. auto. - apply Gt. red. left. auto. + apply LT. red. right. tauto. + apply EQ. red. tauto. + apply GT. red. right. split. apply A.eq_sym. auto. auto. + apply GT. red. left. auto. Qed. End OrderedPair. -- cgit