aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.mli
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2015-12-21 11:37:06 +0100
committerGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-01-11 10:00:45 +0100
commit8a4a8758075e09da298762da1a035a5afac4d88b (patch)
tree4c3c05931f54a5455e6c5a993e839a5ac7716ce8 /kernel/constr.mli
parent730e8b8445c6ff28540aff4a052e19b90159a86d (diff)
COMMENTS: added to the "Names.inductive" and "Names.constructor" types.
Diffstat (limited to 'kernel/constr.mli')
0 files changed, 0 insertions, 0 deletions