From 3d1aa19a70e00dfcb4733b8b478d4865c86e7cd9 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 2 Jul 2020 16:49:16 +0100 Subject: Typo fix --- src/translation/HTLgenproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index e4bbb8f..aec765c 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -2110,7 +2110,7 @@ Section CORRECTNESS. repeat (unfold_match B). inversion B. subst. exploit main_tprog_internal; eauto; intros. rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). - Apply Heqo. symmetry; eapply Linking.match_program_main; eauto. + apply Heqo. symmetry; eapply Linking.match_program_main; eauto. inversion H5. econstructor; split. econstructor. apply (Genv.init_mem_transf_partial TRANSL'); eauto. -- cgit