aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorThéo Zimmermann2018-05-27 14:30:57 +0200
committerThéo Zimmermann2018-05-27 14:31:35 +0200
commit2ba1146e0718568fb5adff418e951261a1e693a4 (patch)
tree06531de235a0cab87d88d05cfd276103dc8eeee5 /kernel/nativecode.ml
parentbba1fe0ac5deb05f3ade9709a8a044d3d6979368 (diff)
Improve subsection on mutual inductive types of the Gallina chapter.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions