diff options
| author | Théo Zimmermann | 2020-05-13 23:36:19 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-13 23:36:19 +0200 |
| commit | d5be454490a7dfb20b7cfffe6c547a2d9ec5f5f1 (patch) | |
| tree | f7028c228cef77d9565f8a6d88cd44ab39002b7d /kernel/type_errors.ml | |
| parent | b1617e188d71e8a27f2888b9e3106373170448d4 (diff) | |
Create a new file on conversion.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions