diff options
| author | Julien Forest | 2018-04-09 21:28:24 +0200 |
|---|---|---|
| committer | Julien Forest | 2018-04-09 21:28:24 +0200 |
| commit | 577738531f607da8e6347ade1dc3767d98aaf863 (patch) | |
| tree | 025d51c19c016dbe31e6104131088770e14de888 /kernel/type_errors.mli | |
| parent | ce3c7ee7cadcab9a194fb37e0d500948078acda0 (diff) | |
change error message in #5147
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions