diff options
| -rw-r--r-- | backend/CSEproof.v | 6 | ||||
| -rw-r--r-- | backend/Constpropproof.v | 4 | ||||
| -rw-r--r-- | backend/Inliningproof.v | 2 | ||||
| -rw-r--r-- | backend/Stackingproof.v | 4 |
4 files changed, 8 insertions, 8 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 209fa40f..5bbb7508 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -1151,7 +1151,7 @@ Proof. econstructor. split. eapply exec_Iload; eauto. - try (rewrite eval_addressing_preserved with (ge1 := ge) by assumption). + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). econstructor; eauto. eapply analysis_correct_1; eauto. simpl; eauto. @@ -1202,7 +1202,7 @@ Proof. { econstructor. split. eapply exec_Iload; eauto. - try (rewrite eval_addressing_preserved with (ge1 := ge) by assumption). + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). econstructor; eauto. eapply analysis_correct_1; eauto. simpl; eauto. @@ -1216,7 +1216,7 @@ Proof. { econstructor. split. eapply exec_Iload_notrap2; eauto. - try (rewrite eval_addressing_preserved with (ge1 := ge) by assumption). + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). econstructor; eauto. eapply analysis_correct_1; eauto. simpl; eauto. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 4d104141..63cfee24 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -476,14 +476,14 @@ Proof. left; econstructor; econstructor; split. eapply exec_Iload; eauto. - try (rewrite eval_addressing_preserved with (ge1 := ge); eassumption). + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). eapply match_states_succ; eauto. apply set_reg_lessdef; auto. } { left; econstructor; econstructor; split. eapply exec_Iload_notrap2; eauto. - try (rewrite eval_addressing_preserved with (ge1 := ge); eassumption). + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). eapply match_states_succ; eauto. apply set_reg_lessdef; auto. } diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index ebc48160..b60c1cb7 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -1025,7 +1025,7 @@ Proof. + left; econstructor; split. eapply plus_one. eapply exec_Iload_notrap2; eauto. - try (rewrite <- P; apply eval_addressing_preserved; assumption). + try (rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved). econstructor; eauto. apply match_stacks_inside_set_reg; auto. apply agree_set_reg; auto. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 19a40e0f..d3fcdb91 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1943,7 +1943,7 @@ Proof. { econstructor; split. apply plus_one. apply exec_Mload with (a:=a') (v:=v'); eauto. - try (rewrite <- A; apply eval_addressing_preserved; assumption). + try (rewrite <- A; apply eval_addressing_preserved; auto; exact symbols_preserved). econstructor; eauto with coqlib. apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto. apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto. @@ -1951,7 +1951,7 @@ Proof. { econstructor; split. apply plus_one. apply exec_Mload_notrap2 with (a:=a'); eauto. - try (rewrite <- A; apply eval_addressing_preserved; assumption). + try (rewrite <- A; apply eval_addressing_preserved; auto; exact symbols_preserved). econstructor; eauto with coqlib. apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto. |