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 /doc/plugin_tutorial | |
| 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.
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions