diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-07-02 16:49:16 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-02 16:49:16 +0100 |
| commit | 3d1aa19a70e00dfcb4733b8b478d4865c86e7cd9 (patch) | |
| tree | f028fab57277e0692bdc92bc3440a7688171c322 | |
| parent | cf19dd40f466691d28f4dfd86211724b700aa217 (diff) | |
| download | vericert-3d1aa19a70e00dfcb4733b8b478d4865c86e7cd9.tar.gz vericert-3d1aa19a70e00dfcb4733b8b478d4865c86e7cd9.zip | |
Typo fix
| -rw-r--r-- | src/translation/HTLgenproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |