diff options
| author | Maxime Dénès | 2017-05-02 16:10:19 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-02 16:35:32 +0200 |
| commit | ba9806a242c7ece41a93181d1fb91279c89794ed (patch) | |
| tree | 2da45092d6005d1ff4aa23c15bcbaf07d7d9cfda /kernel/type_errors.mli | |
| parent | 6156fae91e69d379cfa0263a4c4cafb48da56f85 (diff) | |
Remove dead code in native compiler.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions