diff options
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 9b8dabab..324f1d14 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -230,7 +230,8 @@ Proof. intros; rewrite symbols_preserved; trivial. - (* exec_load *) inv MIB. exists pc'; split; auto; constructor. - apply plus_one. eapply exec_Iload; eauto. + apply plus_one. inv LOAD. + eapply exec_Iload; eauto. all: erewrite <- eval_addressing_preserved; eauto; intros; rewrite symbols_preserved; trivial. - (* exec_store *) |