diff options
| author | Guillaume Melquiond | 2014-10-27 07:21:09 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2014-10-27 07:21:09 +0100 |
| commit | 65c8d91cd4c11b8de44f0b23cd44a3303cd54d4e (patch) | |
| tree | 5b7c97dc58c1b453cd4ba0df838e5cd7a452e309 /kernel/type_errors.ml | |
| parent | cc81b38185b6f558a6908f64cfaa7ee94131bf6c (diff) | |
Fix some typos in comments.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions