aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
authorHugo Herbelin2014-12-08 13:20:29 +0100
committerHugo Herbelin2014-12-08 16:21:24 +0100
commit5e331ad8920bcad2a749904aceebede9dfe7d1a7 (patch)
tree5f80fcbe1b7b39b3562f242f2c522a9ee16945b7 /kernel/nativelambda.mli
parent6b2c23ce5cfd7c0e25e835b5b3cc77909f60e2fe (diff)
This is for documenting and slightly fixing commits 547e97e, c52aea7, 9a34d3e.
As their commit messages suggested it, these commits were not intended to be committed at this time. They are part of a on-going merge of the code of induction and functional induction. Together with the fix here, they are supposingly transparent, semantically speaking.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions