diff options
| author | Vincent Laporte | 2018-10-11 10:04:11 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-16 12:03:46 +0000 |
| commit | 62edc7839bb4b534ea0e82d4ed36f504ad04cb16 (patch) | |
| tree | 35a8d93259a0c33ee3e18b3d4c7e16f64634bd0e /kernel/type_errors.mli | |
| parent | 096d4dd94ff6d506e7a3785da453c21874611cec (diff) | |
[omega] Remove dead code
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions