diff options
| author | Pierre-Marie Pédrot | 2017-07-04 11:36:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-04 11:36:32 +0200 |
| commit | 78f536c7fa1af8a61c3dbc5eafae74ad436958ef (patch) | |
| tree | 4fea2a69455f26d26a2acc4c2dd093d6853b354b /kernel/declareops.ml | |
| parent | 6aeda23a14a5a5dfca259fe99a19d7bcb42d1052 (diff) | |
Removing dead code in Subtyping.
This code was a sketch of what to do when we properly implement module-level
handling of instanciation of definitions by inductive types. It was completely
dead code, called after an error, and somewhat incorrect. Instead of letting
it bitrot, we remove it.
Diffstat (limited to 'kernel/declareops.ml')
0 files changed, 0 insertions, 0 deletions