diff options
| author | Pierre-Marie Pédrot | 2020-01-28 13:49:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-01-28 13:53:12 +0100 |
| commit | 25b85ec88a16de73b942564994b7798d8330f396 (patch) | |
| tree | d0b4014e53d498e9dca5b4acec04186ba4f48a9e /kernel/type_errors.mli | |
| parent | b105077dd42e34f19d0849620fec2837e84b4887 (diff) | |
Remove dead code in Globnames.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions