From 94e0cbc26718fe3fecc58f6f8673f5f8abb0ce31 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 21 Jun 2017 15:12:21 +0200
Subject: [vernac] Remove stale bool parameter from `VernacStartTheoremProof`

`VernacStartTheoremProof` contained a stale bool parameter from 15
years ago, which is unused today.
---
 intf/vernacexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 7c12f9df5d..31ec444707 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -331,7 +331,7 @@ type vernac_expr =
   (* Gallina *)
   | VernacDefinition of
       (locality option * definition_object_kind) * plident * definition_expr
-  | VernacStartTheoremProof of theorem_kind * proof_expr list * bool
+  | VernacStartTheoremProof of theorem_kind * proof_expr list
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
-- 
cgit v1.2.3