diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-29 09:10:29 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-29 09:10:29 +0000 |
commit | 056068abd228fefab4951a61700aa6d54fb88287 (patch) | |
tree | 6bf44526caf535e464e33999641b39032901fa67 /lib/Coqlib.v | |
parent | 34d58b781afec8ecd4afdcf2ab83f1c972338ba9 (diff) | |
download | compcert-kvx-056068abd228fefab4951a61700aa6d54fb88287.tar.gz compcert-kvx-056068abd228fefab4951a61700aa6d54fb88287.zip |
Ported to Coq 8.4pl1. Merge of branches/coq-8.4.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Coqlib.v')
-rw-r--r-- | lib/Coqlib.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 3d5df259..676aa0a5 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -33,7 +33,7 @@ Ltac caseEq name := generalize (refl_equal name); pattern name at -1 in |- *; case name. Ltac destructEq name := - destruct name as []_eqn. + destruct name eqn:?. Ltac decEq := match goal with @@ -393,7 +393,7 @@ Qed. Lemma Zmin_spec: forall x y, Zmin x y = if zlt x y then x else y. Proof. - intros. case (zlt x y); unfold Zlt, Zge; intros. + intros. case (zlt x y); unfold Zlt, Zge; intro z. unfold Zmin. rewrite z. auto. unfold Zmin. caseEq (x ?= y); intro. apply Zcompare_Eq_eq. auto. @@ -404,7 +404,7 @@ Qed. Lemma Zmax_spec: forall x y, Zmax x y = if zlt y x then x else y. Proof. - intros. case (zlt y x); unfold Zlt, Zge; intros. + intros. case (zlt y x); unfold Zlt, Zge; intro z. unfold Zmax. rewrite <- (Zcompare_antisym y x). rewrite z. simpl. auto. unfold Zmax. rewrite <- (Zcompare_antisym y x). @@ -565,7 +565,7 @@ Qed. Lemma Zdivides_trans: forall x y z, (x | y) -> (y | z) -> (x | z). Proof. - intros. inv H. inv H0. exists (q0 * q). ring. + intros x y z [a A] [b B]; subst. exists (a*b); ring. Qed. Definition Zdivide_dec: |