aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorMatthieu Sozeau2015-10-14 15:57:19 +0200
committerMatthieu Sozeau2015-10-14 17:06:49 +0200
commit5b67ba8e1bbd92d4ef7e2adab13bd05e7b55bfd7 (patch)
tree6ddbd6f7a6e61a6b3a20bb0e630738bb723f321f /kernel/nativecode.ml
parentdb80daaf82a08a1475c65f7c82bffb63c7efd27a (diff)
Univs: inductives, remove unneeded test
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions