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 --- backend/Constpropproof.v | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'backend/Constpropproof.v') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 1b906668..cd757cdf 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -199,9 +199,9 @@ Lemma eval_static_load_sound: val_match_approx ge sp (eval_static_load gapp chunk addr) v. Proof. intros. unfold eval_static_load. destruct addr; simpl; auto. - destruct (gapp!i) as [il|]_eqn; auto. + destruct (gapp!i) as [il|] eqn:?; auto. red in H1. subst vaddr. unfold symbol_address in H. - destruct (Genv.find_symbol ge i) as [b'|]_eqn; simpl in H; try discriminate. + destruct (Genv.find_symbol ge i) as [b'|] eqn:?; simpl in H; try discriminate. exploit H0; eauto. intros [A [B C]]. eapply eval_load_init_sound; eauto. red; auto. @@ -290,7 +290,7 @@ Proof. \/ id0 <> id /\ ga!id0 = Some il). destruct gd. rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); [discriminate|auto]. - destruct (gvar_readonly v && negb (gvar_volatile v)) as []_eqn. + destruct (gvar_readonly v && negb (gvar_volatile v)) eqn:?. rewrite PTree.gsspec in H0. destruct (peq id0 id). inv H0. left. split; auto. destruct v; simpl in *. @@ -455,10 +455,10 @@ Lemma match_successor_rec: Proof. induction n; simpl; intros. apply match_pc_base. - destruct (fn_code f)!pc as [i|]_eqn; try apply match_pc_base. + destruct (fn_code f)!pc as [i|] eqn:?; try apply match_pc_base. destruct i; try apply match_pc_base. eapply match_pc_nop; eauto. - destruct (eval_static_condition c (approx_regs app l)) as [b|]_eqn. + destruct (eval_static_condition c (approx_regs app l)) as [b|] eqn:?. eapply match_pc_cond; eauto. apply match_pc_base. Qed. @@ -607,7 +607,7 @@ Proof. assert (MATCH'': regs_match_approx sp (analyze gapp f) # pc' rs # res <- v). eapply analyze_correct_1 with (pc := pc); eauto. simpl; auto. unfold transfer; rewrite H. auto. - destruct (const_for_result a) as [cop|]_eqn; intros. + destruct (const_for_result a) as [cop|] eqn:?; intros. (* constant is propagated *) left; econstructor; econstructor; split. eapply exec_Iop; eauto. @@ -640,7 +640,7 @@ Proof. eapply approx_regs_val_list; eauto. assert (VM2: val_match_approx ge sp ap2 v). eapply eval_static_load_sound; eauto. - destruct (const_for_result ap2) as [cop|]_eqn; intros. + destruct (const_for_result ap2) as [cop|] eqn:?; intros. (* constant-propagated *) left; econstructor; econstructor; split. eapply exec_Iop; eauto. eapply const_for_result_correct; eauto. @@ -708,7 +708,7 @@ Proof. (* Ibuiltin *) rename pc'0 into pc. Opaque builtin_strength_reduction. - destruct (builtin_strength_reduction ef args (approx_regs (analyze gapp f)#pc args)) as [ef' args']_eqn. + destruct (builtin_strength_reduction ef args (approx_regs (analyze gapp f)#pc args)) as [ef' args'] eqn:?. generalize (builtin_strength_reduction_correct ge sp (analyze gapp f)!!pc rs MATCH2 ef args (approx_regs (analyze gapp f) # pc args) _ _ _ _ (refl_equal _) H0). rewrite Heqp. intros P. @@ -732,7 +732,7 @@ Opaque builtin_strength_reduction. destruct (cond_strength_reduction cond args (approx_regs (analyze gapp f) # pc args)) as [cond' args']. intros EV1 TCODE. left; exists O; exists (State s' (transf_function gapp f) sp (if b then ifso else ifnot) rs' m'); split. - destruct (eval_static_condition cond (approx_regs (analyze gapp f) # pc args)) as []_eqn. + destruct (eval_static_condition cond (approx_regs (analyze gapp f) # pc args)) eqn:?. assert (eval_condition cond rs ## args m = Some b0). eapply eval_static_condition_correct; eauto. eapply approx_regs_val_list; eauto. assert (b = b0) by congruence. subst b0. @@ -758,7 +758,7 @@ Opaque builtin_strength_reduction. rename pc'0 into pc. assert (A: (fn_code (transf_function gapp f))!pc = Some(Ijumptable arg tbl) \/ (fn_code (transf_function gapp f))!pc = Some(Inop pc')). - TransfInstr. destruct (approx_reg (analyze gapp f) # pc arg) as []_eqn; auto. + TransfInstr. destruct (approx_reg (analyze gapp f) # pc arg) eqn:?; auto. generalize (MATCH2 arg). unfold approx_reg in Heqt. rewrite Heqt. rewrite H0. simpl. intro EQ; inv EQ. rewrite H1. auto. assert (B: rs'#arg = Vint n). -- cgit