From d6c6c87d61dc10b1acaeb056975675c7e523f1ef Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 5 Jul 2020 02:46:11 +0100
Subject: Remove admitted in mis_stepp_Vdecl

---
 src/translation/Veriloggenproof.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'src/translation/Veriloggenproof.v')

diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v
index 3052d03..ee0aa64 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/translation/Veriloggenproof.v
@@ -195,8 +195,12 @@ Section CORRECTNESS.
 
   Lemma mis_stepp_decl :
     forall l asr asa f,
-      mis_stepp f asr asa l asr asa.
-  Admitted.
+      mis_stepp f asr asa (map Vdeclaration l) asr asa.
+  Proof.
+    induction l.
+    - intros. constructor.
+    - intros. simplify. econstructor. constructor. auto.
+  Qed.
 
   Let ge : HTL.genv := Globalenvs.Genv.globalenv prog.
   Let tge : genv := Globalenvs.Genv.globalenv tprog.
-- 
cgit