diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-02-05 11:38:04 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-02-05 11:38:04 +0100 |
| commit | b5692de75c9c23105bac4a0b2510d868bb7c2631 (patch) | |
| tree | 5d6489d2bc117be483997eef025a7e93503d1e76 /cfrontend/SimplExprproof.v | |
| parent | abb704f93055a572a5078e04c5212ff051309730 (diff) | |
| download | compcert-kvx-b5692de75c9c23105bac4a0b2510d868bb7c2631.tar.gz compcert-kvx-b5692de75c9c23105bac4a0b2510d868bb7c2631.zip | |
Restart the name generator at first_unused_ident for every function.
This makes it easier to generate semi-meaningful names for compiler-generated temporaries in the clightgen tool.
Diffstat (limited to 'cfrontend/SimplExprproof.v')
| -rw-r--r-- | cfrontend/SimplExprproof.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 8f06e777..0c7c9ce7 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -2235,8 +2235,9 @@ Proof. econstructor; split. econstructor. exploit Genv.init_mem_match; eauto. - change (Genv.globalenv tprog) with (genv_genv tge). rewrite symbols_preserved. - rewrite <- H4; simpl; eauto. + change (Genv.globalenv tprog) with (genv_genv tge). + rewrite symbols_preserved. rewrite <- H4; simpl. + rewrite (transform_partial_program_main _ _ EQ). eauto. eexact FIND. rewrite <- H3. apply type_of_fundef_preserved. auto. constructor. auto. constructor. |