diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-01-25 16:52:00 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-02-01 16:20:16 +0000 |
| commit | 5b8b60508d74bfe5e436ce182889ad8ee6ca3983 (patch) | |
| tree | 3a9bdfb906444e1f041af3e09df0cc49f911839b /vernac/lemmas.mli | |
| parent | e42f575b22ff2d2a69951227e8c2dd67fd0ab3ee (diff) | |
[vernac] Mutual theorems (VernacStartTheoremProof) always have names
Diffstat (limited to 'vernac/lemmas.mli')
| -rw-r--r-- | vernac/lemmas.mli | 2 |
1 files changed, 2 insertions, 0 deletions
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 *) |