aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-07-06 14:31:13 +0200
committerMaxime Dénès2017-07-06 14:31:13 +0200
commit307f08d2ad2aca5d48441394342af4615810d0c7 (patch)
tree85f96651d250d107762473ca5d5f320f251c37a3 /kernel/inductive.ml
parent1111aeb445261af9e74770c0fe3bfd0ffd4930e2 (diff)
parent78f536c7fa1af8a61c3dbc5eafae74ad436958ef (diff)
Merge PR #853: Clean 'with Definition' implementation.
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions