aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling
diff options
context:
space:
mode:
Diffstat (limited to 'scheduling')
-rw-r--r--scheduling/BTLtoRTLproof.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 2e3c5cd8..c342d076 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -231,9 +231,9 @@ Proof.
- (* exec_load *)
inv MIB. exists pc'; split; auto; constructor.
apply plus_one. inversion LOAD; subst.
- + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
- rewrite <- EVAL. erewrite <- eval_addressing_preserved; eauto.
- intros; rewrite symbols_preserved; trivial.
+ + try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto;
+ rewrite <- EVAL; erewrite <- eval_addressing_preserved; eauto;
+ intros; rewrite symbols_preserved; trivial).
+ destruct (eval_addressing) eqn:EVAL in LOAD0.
* specialize (LOAD0 v).
eapply exec_Iload; eauto. eapply has_loaded_default; eauto.