aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
authorHugo Herbelin2014-12-07 17:59:28 +0100
committerHugo Herbelin2016-01-14 13:12:01 +0100
commitc7a7d55e0dc47a097bf0d0c8897bc490ce55577b (patch)
treed1305711dd507b512ba97f0c57b85cabcbff1579 /kernel/nativelambda.mli
parent8e06c02845df0f1243ca260c7707cc912734c704 (diff)
Update in the documentation of parts of the code of destruct/induction.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions