diff options
| author | Guillaume Melquiond | 2016-06-23 10:25:15 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-06-23 10:25:15 +0200 |
| commit | 7ae226092719b26f71b675d6ceb211801349bc00 (patch) | |
| tree | a88d95f501cff92c97d4004ef47548d9ade25ac1 /kernel/nativecode.ml | |
| parent | 0fa8b96c243e0915477866b094735ecaaaac6ef6 (diff) | |
Remove extraction-specific code from the checker.
It seems like this code was copy-pasted from kernel/inductive.ml. It was
already dubious enough in the kernel. It feels completely wrong in the
checker.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions