diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Deadcodeproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index be64a1a7..52332a82 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -823,7 +823,7 @@ Ltac UseTransfer := intros (tv & P & Q). econstructor; split. try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; - [ rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved | eauto]). + try (rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved; fail); eauto). eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. @@ -851,7 +851,7 @@ Ltac UseTransfer := { econstructor; split. try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; - erewrite eval_addressing_preserved with (ge1 := ge); [ assumption | exact symbols_preserved]). + try (rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved; fail); eauto). eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. |