diff options
| author | Pierre-Marie Pédrot | 2020-06-16 15:30:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-16 15:31:48 +0200 |
| commit | 31cbaf0fe258438948ba9611d599dc456c313ddd (patch) | |
| tree | c3b4dfb4bf84a3c2445299f64027537621580c2b /kernel/type_errors.ml | |
| parent | 948d8bc64ebfa6371a0dd785c119b5223293ba2b (diff) | |
Code simplification in Autorewrite.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions