diff options
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 2a33fa1c..a6fc73aa 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -679,8 +679,7 @@ Proof. apply WTRS. -- econstructor. split. + eapply exec_Ireturn; try eassumption. - * erewrite transf_function_at by eauto. simpl. - admit. + * TR_AT; reflexivity. * rewrite stacksize_preserved with (f:=f); eauto. + econstructor; eauto. simpl. trivial. |