diff options
| author | Pierre-Marie Pédrot | 2019-02-05 16:03:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-05 16:04:39 +0100 |
| commit | 1e4d643b8bb0f516651294d8881711720e349b85 (patch) | |
| tree | 570754c65f530576aa15c738a0b375c55fa17732 /kernel/type_errors.ml | |
| parent | b307529a3888ab632b7076a793904d150d263eac (diff) | |
Remove the comment fields of locations.
They didn't seem to be used at all.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions