From 98ec44d9d96e7e94896eea9ac054a0188be7b6dd Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Nov 2021 11:17:10 +0100 Subject: bugfix --- backend/Deadcodeproof.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend') 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. -- cgit