diff options
| author | Pierre-Marie Pédrot | 2019-12-03 18:37:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-11 16:49:26 +0100 |
| commit | abcae4e339cc33660ba53c5d10066392ed414fa4 (patch) | |
| tree | 890ce4ed93955c8346d1bab551e2bb003719825f /pretyping/pretype_errors.mli | |
| parent | 9522f39615e7f20c2ce4e1d4274ef475fdcca26e (diff) | |
Remove the reliance of ring objects on the named part.
This was just dead code.
Diffstat (limited to 'pretyping/pretype_errors.mli')
0 files changed, 0 insertions, 0 deletions