Remove Show Proof in InfiniteToFinite.v

vellvm · Apr 15, 2024 · 789ba6c · 789ba6c
1 parent 954dc95
commit 789ba6c
Showing 1 changed file with 0 additions and 2 deletions.
diff --git 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 *)