diff options
| author | Pierre-Marie Pédrot | 2017-09-08 02:32:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-08 02:32:54 +0200 |
| commit | 2b66bf0083fd85cf2fc983dbca75b848194f897f (patch) | |
| tree | ec28528453f9a4719529406b3c186a8eb30dd093 /kernel/type_errors.mli | |
| parent | 9820b2c72cbf2da61cf44456334b38683799fd58 (diff) | |
Fix coq/ltac2#27: ... is not a particularly helpful printing of an error message.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions