diff options
| author | Maxime Dénès | 2020-06-16 00:09:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-06-23 12:09:04 +0200 |
| commit | f67a09a9201916066ed8c9ece073232317e75a8d (patch) | |
| tree | 5a7af13f9d800ce5c819bc32e58b99d9e42af6c6 /kernel/type_errors.ml | |
| parent | 700918ada1c864c900bdc065d39c4b16d2a47500 (diff) | |
Fix #4459 by improving `par:` error message
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions