diff options
| author | Maxime Dénès | 2016-07-04 15:04:30 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-07-04 15:04:30 +0200 |
| commit | c22f6694bac3479426cf179839430d9d8675e456 (patch) | |
| tree | f72f681336b8a0a80b671ac338d0382f3775ea4f /kernel/type_errors.ml | |
| parent | 0eb08b70f0c576e58912c1fc3ef74f387ad465be (diff) | |
Mention more fixes in CHANGES before we release pl2.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions