From 056068abd228fefab4951a61700aa6d54fb88287 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jan 2013 09:10:29 +0000 Subject: 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 --- lib/Coqlib.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'lib/Coqlib.v') 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: -- cgit