diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 19:10:14 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-31 19:10:14 +0200 |
| commit | 47f10ace41f8fb8ef818dbf1ca1d846b91b753c9 (patch) | |
| tree | c84e7e08c97935a0fb5a1a96a4d6732bd71adb08 /backend/CSE2proof.v | |
| parent | 6ec981b26bd3f3d6c379ec48fd6ac6931a86bff5 (diff) | |
| download | compcert-kvx-47f10ace41f8fb8ef818dbf1ca1d846b91b753c9.tar.gz compcert-kvx-47f10ace41f8fb8ef818dbf1ca1d846b91b753c9.zip | |
forgot an 'Admitted'
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index fc980fb4..309ccce1 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -1680,7 +1680,7 @@ Proof. econstructor; split. eapply exec_return; eauto. constructor; auto. -Admitted. +Qed. Lemma transf_initial_states: |