diff options
| author | Vincent Laporte | 2018-10-11 13:04:24 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-16 12:03:50 +0000 |
| commit | 8bba1951cab1088d057aac68425271191b7c296c (patch) | |
| tree | ca4ac7edce79bab084f9acb6fe5d4015a24a0cbc /kernel/type_errors.mli | |
| parent | 62edc7839bb4b534ea0e82d4ed36f504ad04cb16 (diff) | |
[btauto] Remove dead code
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions