diff options
Diffstat (limited to 'backend/CleanupLabelsproof.v')
| -rw-r--r-- | backend/CleanupLabelsproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index a498a654..e92be2b4 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -315,7 +315,7 @@ Proof. econstructor; eauto with coqlib. (* external function *) left; econstructor; split. - econstructor; eauto. eapply external_call_symbols_preserved'; eauto. apply senv_preserved. + econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto with coqlib. (* return *) inv H3. inv H1. left; econstructor; split. @@ -341,7 +341,7 @@ Lemma transf_final_states: forall st1 st2 r, match_states st1 st2 -> final_state st1 r -> final_state st2 r. Proof. - intros. inv H0. inv H. inv H6. econstructor; eauto. + intros. inv H0. inv H. inv H5. econstructor; eauto. Qed. Theorem transf_program_correct: |