diff options
| author | Hugo Herbelin | 2020-01-20 08:45:35 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-01-21 00:20:49 +0100 |
| commit | 9d88395fd25031445d463648e81c600df179cbc6 (patch) | |
| tree | 45dcb8adee2088a034ade2af398bb5c79f93485b /kernel/type_errors.mli | |
| parent | 7e98fc9ee477505e3bb6d2c91a3d5d46d5fffbc5 (diff) | |
Typo in an anomaly message.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions