aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-08-19 18:30:50 +0200
committerPierre-Marie Pédrot2015-08-19 18:31:30 +0200
commit3696238f8dd435426080ba7d1b40c8ceacacb6ee (patch)
tree56dbe457b04827c601152e071baa513930db7aed /kernel/nativelambda.ml
parent00f333fe7ae2e7bd4ced4be78d24737e62a7b369 (diff)
Documentation by giving a name to a large type.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions