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 --- ia32/Asmgenproof.v | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) (limited to 'ia32/Asmgenproof.v') diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 3d0c57f5..d618d44d 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -1122,7 +1122,8 @@ Proof. intros. simpl in H2. destruct (transl_cond_correct tge tf cond args _ _ rs m' H2) as [rs' [A [B C]]]. - unfold PregEq.t in B; rewrite EC in B. + rewrite EC in B (* 8.4 *) + || (unfold PregEq.t in B; rewrite EC in B) (* 8.3 *). destruct (testcond_for_condition cond); simpl in *. (* simple jcc *) exists (Pjcc c1 lbl); exists k; exists rs'. @@ -1130,8 +1131,8 @@ Proof. split. eapply agree_exten_temps; eauto. simpl. rewrite B. auto. (* jcc; jcc *) - destruct (eval_testcond c1 rs') as [b1|]_eqn; - destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B. + destruct (eval_testcond c1 rs') as [b1|] eqn:?; + destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B. destruct b1. (* first jcc jumps *) exists (Pjcc c1 lbl); exists (Pjcc c2 lbl :: k); exists rs'. @@ -1147,8 +1148,8 @@ Proof. simpl. rewrite eval_testcond_nextinstr. rewrite Heqo0. destruct b2; auto || discriminate. (* jcc2 *) - destruct (eval_testcond c1 rs') as [b1|]_eqn; - destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B. + destruct (eval_testcond c1 rs') as [b1|] eqn:?; + destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B. destruct (andb_prop _ _ H4). subst. exists (Pjcc2 c1 c2 lbl); exists k; exists rs'. split. eexact A. @@ -1169,7 +1170,8 @@ Proof. left; eapply exec_straight_steps; eauto. intros. simpl in H0. destruct (transl_cond_correct tge tf cond args _ _ rs m' H0) as [rs' [A [B C]]]. - unfold PregEq.t in B; rewrite EC in B. + rewrite EC in B (* 8.4 *) + || (unfold PregEq.t in B; rewrite EC in B) (* 8.3 *). destruct (testcond_for_condition cond); simpl in *. (* simple jcc *) econstructor; split. @@ -1178,8 +1180,8 @@ Proof. split. apply agree_nextinstr. eapply agree_exten_temps; eauto. simpl; congruence. (* jcc ; jcc *) - destruct (eval_testcond c1 rs') as [b1|]_eqn; - destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B. + destruct (eval_testcond c1 rs') as [b1|] eqn:?; + destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B. destruct (orb_false_elim _ _ H2); subst. econstructor; split. eapply exec_straight_trans. eexact A. @@ -1188,8 +1190,8 @@ Proof. split. apply agree_nextinstr. apply agree_nextinstr. eapply agree_exten_temps; eauto. simpl; congruence. (* jcc2 *) - destruct (eval_testcond c1 rs') as [b1|]_eqn; - destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B. + destruct (eval_testcond c1 rs') as [b1|] eqn:?; + destruct (eval_testcond c2 rs') as [b2|] eqn:?; inv B. exists (nextinstr rs'); split. eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl. -- cgit