From b5692de75c9c23105bac4a0b2510d868bb7c2631 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 5 Feb 2016 11:38:04 +0100 Subject: 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. --- cfrontend/SimplExprproof.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'cfrontend/SimplExprproof.v') 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. -- cgit