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 /backend/Selectionproof.v | |
| parent | 34d58b781afec8ecd4afdcf2ab83f1c972338ba9 (diff) | |
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 'backend/Selectionproof.v')
| -rw-r--r-- | backend/Selectionproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
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. |