diff options
| author | Emilio Jesus Gallego Arias | 2018-05-20 21:15:44 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-27 17:13:32 +0200 |
| commit | 1cd62aa20ba3f9fb206f2926c8e47dd463dee863 (patch) | |
| tree | 5bd59b5a707a0e1aec7a34aa66ecda1136dc0607 /doc/plugin_tutorial/tuto2 | |
| parent | e15c228709351f5001f6a10765a816cebcf900cc (diff) | |
Adapt to coq/coq#7558.
Trivial renaming of the vernacular parsing entry point.
Diffstat (limited to 'doc/plugin_tutorial/tuto2')
0 files changed, 0 insertions, 0 deletions