aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorThéo Zimmermann2020-05-13 20:11:07 +0200
committerThéo Zimmermann2020-05-13 20:11:07 +0200
commit75d32b4abaeefb505d62ae201c0edc555f473396 (patch)
treec40785d0003b5e3992ba916f1c0a6f0953453cd6 /kernel/type_errors.ml
parent485c5a1590daaee61a4ca7801fd6de3ee7489e6c (diff)
Create new file on Inductive types.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions