diff options
| author | Arnaud Spiwack | 2014-02-25 16:46:45 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-02-25 17:16:56 +0100 |
| commit | 2eaf2b1093c08304d34ba898d38343f20e7538e3 (patch) | |
| tree | 6fd16c4e34fbf3d3d7b498a33895e35341383931 /kernel/type_errors.mli | |
| parent | ce9adc468df630e0fa1a0888fcff1fafc5b183ed (diff) | |
Tacinterp: fewer enterl still.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions