diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-06-05 13:39:59 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-06-05 13:39:59 +0000 |
| commit | 615fb53c13f2407a0b6b470bbdf8e468fc4a1d78 (patch) | |
| tree | ec5f45b6546e19519f59b1ee0f42955616ca1b98 /backend/Tailcallproof.v | |
| parent | d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb (diff) | |
| download | compcert-kvx-615fb53c13f2407a0b6b470bbdf8e468fc4a1d78.tar.gz compcert-kvx-615fb53c13f2407a0b6b470bbdf8e468fc4a1d78.zip | |
Adapted to work with Coq 8.2-1v1.4.1
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Tailcallproof.v')
| -rw-r--r-- | backend/Tailcallproof.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 8e97e1a4..791db374 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -574,8 +574,8 @@ Proof. exploit loadv_lessdef; eauto. intros [v' [LOAD' VLD]]. left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' (rs'#dst <- v') m'); split. - eapply exec_Iload; eauto. rewrite <- ADDR'. - apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload with (a := a'). eauto. rewrite <- ADDR'. + apply eval_addressing_preserved. exact symbols_preserved. eauto. econstructor; eauto. apply regset_set; auto. (* store *) @@ -586,8 +586,8 @@ Proof. exploit storev_lessdef. 4: eexact H1. eauto. eauto. apply RLD. intros [m'1 [STORE' MLD']]. left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' rs' m'1); split. - eapply exec_Istore; eauto. rewrite <- ADDR'. - apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Istore with (a := a'). eauto. rewrite <- ADDR'. + apply eval_addressing_preserved. exact symbols_preserved. eauto. destruct a; simpl in H1; try discriminate. econstructor; eauto. eapply match_stacksize_store; eauto. |