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/Selectionproof.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backend/Selectionproof.v') diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 09dc0ff..0269438 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -166,10 +166,10 @@ Lemma classify_call_correct: end. Proof. unfold classify_call; intros. - destruct (expr_is_addrof_ident a) as [id|]_eqn. + destruct (expr_is_addrof_ident a) as [id|] eqn:?. exploit expr_is_addrof_ident_correct; eauto. intros EQ; subst a. inv H. inv H2. - destruct (Genv.find_symbol ge id) as [b|]_eqn. + destruct (Genv.find_symbol ge id) as [b|] eqn:?. rewrite Genv.find_funct_find_funct_ptr in H0. rewrite H0. destruct fd. exists b; auto. @@ -567,7 +567,7 @@ Proof. apply call_cont_commut; eauto. rewrite H. destruct (find_label lbl (sel_stmt ge (Cminor.fn_body f)) (call_cont k'0)) - as [[s'' k'']|]_eqn; intros; try contradiction. + as [[s'' k'']|] eqn:?; intros; try contradiction. destruct H0. left; econstructor; split. econstructor; eauto. -- cgit v1.2.3