diff options
| author | Hugo Herbelin | 2016-04-13 00:46:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-16 17:43:27 +0200 |
| commit | d28f2685615450c3c807764ce12bfdbe62450a01 (patch) | |
| tree | 7910f577a092b7a6c0fe983f6f64f01b79ffc20f /kernel/type_errors.ml | |
| parent | 16b13e1aeac9559fc43939aa6d1d3f13a08daa14 (diff) | |
Printing notations as parsed.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions