aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
diff options
context:
space:
mode:
authorHugo Herbelin2015-02-27 14:23:02 +0100
committerHugo Herbelin2015-02-27 16:59:29 +0100
commit1388171a48d8e068d5d0ed93b74faa4ac7da5f7f (patch)
tree5bfe6521f80fa3b0dc49431aa2e3e34aec77a5bb /kernel/inductive.ml
parent1019a654a8262ee1b8b1e1a7f652a7e3d111d20e (diff)
Fixing typo resulting in wrong printing of return clauses for
inductive types with let-in in arity.
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions