aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorThéo Zimmermann2020-05-13 20:11:07 +0200
committerThéo Zimmermann2020-05-13 20:11:07 +0200
commit75d32b4abaeefb505d62ae201c0edc555f473396 (patch)
treec40785d0003b5e3992ba916f1c0a6f0953453cd6 /kernel/nativecode.mli
parent485c5a1590daaee61a4ca7801fd6de3ee7489e6c (diff)
Create new file on Inductive types.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions