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 /kernel/type_errors.mli | |
| parent | e15c228709351f5001f6a10765a816cebcf900cc (diff) | |
Adapt to coq/coq#7558.
Trivial renaming of the vernacular parsing entry point.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions