From 47f10ace41f8fb8ef818dbf1ca1d846b91b753c9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 19:10:14 +0200 Subject: forgot an 'Admitted' --- backend/CSE2proof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/CSE2proof.v') 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: -- cgit