aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--backend/CSE2proof.v2
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: