diff options
| author | Julien Forest | 2018-04-09 12:02:13 +0200 |
|---|---|---|
| committer | Julien Forest | 2018-04-09 12:02:13 +0200 |
| commit | ce3c7ee7cadcab9a194fb37e0d500948078acda0 (patch) | |
| tree | e4daf6404db0d3d287456e2532efb75bfa90a0ab /kernel/type_errors.ml | |
| parent | d28546e681b6436386ab9a1e8907068348a1cff0 (diff) | |
removing uggly error message of #5147
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions