diff options
| author | Hugo Herbelin | 2020-11-16 14:18:20 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-16 14:18:20 +0100 |
| commit | 5ded9cae169799a51aa713c9f2807d356a37fb58 (patch) | |
| tree | b032cdae0629912df49aac8d3fee76ec8f3599cc /kernel/type_errors.ml | |
| parent | eae015fa8aadab229a056eb869e2b926fa6c9dc2 (diff) | |
Add changelog for #13337.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions