aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
authorGaëtan Gilbert2017-11-11 22:02:20 +0100
committerGaëtan Gilbert2018-02-11 22:28:39 +0100
commita9240de59f6822f55a57d0e6453bd0635795720d (patch)
tree18e2a5c20b7773dcf7edaf6f68ce4d854cabf570 /kernel/nativelambda.mli
parentd81ea7705cd60b6bcb1de07282860228a23b68ac (diff)
Print inductive cumulativity info in About.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions