From 789ba6c778ed63d8073b87ad3cbc7dfdf6f47d0b Mon Sep 17 00:00:00 2001
From: Calvin Beck <hobbes@ualberta.ca>
Date: Mon, 15 Apr 2024 14:29:31 -0400
Subject: [PATCH] Remove Show Proof in InfiniteToFinite.v

---
 src/coq/Semantics/InfiniteToFinite.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/coq/Semantics/InfiniteToFinite.v b/src/coq/Semantics/InfiniteToFinite.v
index 31127a98..e8cf7d4e 100644
--- a/src/coq/Semantics/InfiniteToFinite.v
+++ b/src/coq/Semantics/InfiniteToFinite.v
@@ -32671,8 +32671,6 @@ cofix CIH
         inversion H0; subst.
         exact (LLVMEvents.raise "").
       }
-
-      Show Proof.
   Defined.
 
   (* This is used to construct get_inf_tree_L4 *)