diff options
| author | Hugo Herbelin | 2018-10-06 22:13:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-07 19:55:18 +0200 |
| commit | 8ba19283c5c21bfa4679934a796050a0d3ab0696 (patch) | |
| tree | f3bf8f730c297efcbffb7190d2a72ecec4781263 /kernel/type_errors.ml | |
| parent | f4d0789f1b1af3bc831a6e3e536210dbfe30692e (diff) | |
Adding missing header in functional_principles_types.ml.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions