diff options
| author | Emilio Jesus Gallego Arias | 2020-05-22 03:36:36 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-26 18:28:08 +0200 |
| commit | e1a3216700427853bd5fba36e84da78b46b6cea0 (patch) | |
| tree | 1cfae455f1f70ac6f10a2577a417088571ece551 /kernel/type_errors.ml | |
| parent | d9d4dcb41d8a63b7d535200b68bcbef4a38993df (diff) | |
[declare] Nit on errors.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions