diff options
| author | Emilio Jesus Gallego Arias | 2016-10-10 17:09:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-02-14 23:29:53 +0100 |
| commit | 0ca1717a3a1243d3fd905bb2f6c3d427f1f98dc6 (patch) | |
| tree | d5e2749e9fe2745ad806e86285df9cefe818f63b /kernel/type_errors.ml | |
| parent | 4fd59386e7f60d16bfe9858c372b354d422ac0b6 (diff) | |
[misc] Remove unused binding.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions