diff options
| author | Pierre-Marie Pédrot | 2018-09-07 13:44:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-07 13:44:44 +0200 |
| commit | 2139ee422754f4c3e039f7d3e3316fea47123b5c (patch) | |
| tree | c2f6c3c63ebb26f0f66ecbc2d4556048761ce5bf /kernel/type_errors.mli | |
| parent | 07c3905c30590c93f1b173833087bbd1df364227 (diff) | |
| parent | f6ed48098636f11362945d380bbe8cb71a9ab2ee (diff) | |
Merge PR #8423: coqpp: allow DEPRECATED when declaring tactics
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions