diff options
| author | Emilio Jesus Gallego Arias | 2020-03-02 02:17:42 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-19 17:18:54 -0400 |
| commit | aa7a5ab6bdabd4205b64115fd2d803d2a06590a0 (patch) | |
| tree | 96f3324e7ec26819d5005095d2ef375182d3f165 | |
| parent | cdf961716bc825f362ea98b73be8e6a6201d52f0 (diff) | |
[lemmas] Fix comment on public API
After we moved `start_lemma_com` to `vernacentries` the comment on
`start_lemma_with_initialization` needs update.
| -rw-r--r-- | vernac/lemmas.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 79fdfe37de..67230e30f7 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -95,7 +95,7 @@ val start_dependent_lemma type lemma_possible_guards = int list list -(** Pretty much internal, only used in ComFixpoint *) +(** Pretty much internal, used by the Lemma / Fixpoint vernaculars *) val start_lemma_with_initialization : ?hook:DeclareDef.Hook.t -> poly:bool |