From ce3adde4b50ba04430a1cf0ffb0ea85168091746 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 8 Oct 2021 23:03:21 +0100
Subject: End section in Abstr.v

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

diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index 9bed783..957e265 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -736,6 +736,8 @@ Section CORRECT.
 Qed.*)
   Abort.
 
+End CORRECT.
+
 Lemma get_empty:
   forall r, empty#r = Psingle (Ebase r).
 Proof.
-- 
cgit