From 5b8b60508d74bfe5e436ce182889ad8ee6ca3983 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Thu, 25 Jan 2018 16:52:00 +0000
Subject: [vernac] Mutual theorems (VernacStartTheoremProof) always have names

---
 vernac/lemmas.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'vernac/lemmas.mli')

diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index ca92e856b..126dcd8b0 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -52,6 +52,8 @@ val standard_proof_terminator :
   Proof_global.lemma_possible_guards -> unit declaration_hook ->
     Proof_global.proof_terminator
 
+val fresh_name_for_anonymous_theorem : unit -> Id.t
+
 (** {6 ... } *)
 
 (** A hook the next three functions pass to cook_proof *)
-- 
cgit v1.2.3