diff options
| author | Maxime Dénès | 2014-07-22 15:56:32 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-07-22 18:05:01 -0400 |
| commit | 283ce711d67d18889e0e4acf51d9ef15a35e6ab7 (patch) | |
| tree | c92b2f4e3ec7804c27b2b6015c9002446af2cc57 /checker/type_errors.ml | |
| parent | d82edc74c1b2c1ac735959eb12f2d3c70da17757 (diff) | |
Minor cleaning.
Diffstat (limited to 'checker/type_errors.ml')
0 files changed, 0 insertions, 0 deletions