diff options
Diffstat (limited to 'backend/Deadcodeproof.v')
| -rw-r--r-- | backend/Deadcodeproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index fa402e9f..3f0c5a4c 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -1101,7 +1101,7 @@ Proof. exists (Callstate nil tf nil m0); split. econstructor; eauto. eapply (Genv.init_mem_match TRANSF); eauto. - replace (prog_main tprog) with (prog_main prog). + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. symmetry; eapply match_program_main; eauto. rewrite <- H3. eapply sig_function_translated; eauto. |