diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-04 15:08:29 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-04 15:08:29 +0000 |
| commit | 73729d23ac13275c0d28d23bc1b1f6056104e5d9 (patch) | |
| tree | e3044ce75edb30377bd8c87356b7617eba5ed223 /lib/Ordered.v | |
| parent | c79434827bf2bd71f857f4471f7bbf381fddd189 (diff) | |
| download | compcert-kvx-73729d23ac13275c0d28d23bc1b1f6056104e5d9.tar.gz compcert-kvx-73729d23ac13275c0d28d23bc1b1f6056104e5d9.zip | |
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
Diffstat (limited to 'lib/Ordered.v')
| -rw-r--r-- | lib/Ordered.v | 24 |
1 files changed, 12 insertions, 12 deletions
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. |