From deb5fabefb2b67d46f1df6efc08c217c5197338a Mon Sep 17 00:00:00 2001
From: Michalis Pardalos <m.pardalos@gmail.com>
Date: Tue, 18 May 2021 21:24:33 +0100
Subject: Qed on top-level correctness lemma

---
 src/hls/HTLgenproof.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/hls')

diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index aa5e7e1..7d71819 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -2914,8 +2914,8 @@ Section CORRECTNESS.
         match_states ge S1 R1 ->
         exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states ge S2 R2.
   Proof.
-    induction 1; try (eauto with htlproof; intros; inv_state).
-  Admitted.
+    induction 1; eauto with htlproof; try solve [ intros; inv_state ].
+  Qed.
 
   Hint Resolve transl_step_correct : htlproof.
 
-- 
cgit