diff options
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 9e0ad909..f9c7b400 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -1527,7 +1527,10 @@ Proof. assert (eval_addressing tge sp addr rs ## args = Some a). rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. eapply exec_Istore; eauto. - rewrite (subst_args_ok' sp m); assumption. + - rewrite (subst_args_ok' sp m) by assumption. + eassumption. + - rewrite (subst_arg_ok' sp m) by assumption. + eassumption. } constructor; auto. |