diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-14 08:05:37 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-14 08:05:37 +0100 |
| commit | c875003382b2741557d6657ab4611a4c4fa8e9c6 (patch) | |
| tree | feee8dabb698ac34297ee890074e7a894c42ec12 /backend/CSE3proof.v | |
| parent | 74fef42251167061e7fd863ac2bb06bb6e58d3d4 (diff) | |
| download | compcert-kvx-c875003382b2741557d6657ab4611a4c4fa8e9c6.tar.gz compcert-kvx-c875003382b2741557d6657ab4611a4c4fa8e9c6.zip | |
Ireturn
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. |