aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.mli
diff options
context:
space:
mode:
authorGravatar Amin Timany <amintimany@gmail.com>2017-03-28 19:24:02 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-16 04:45:18 +0200
commit44f462aa380de847452c0809d15c86649d5d6a7a (patch)
tree840d369425f4b5fc2f6c41fb8dba91e90e8cfbc4 /kernel/univ.mli
parent1d3703be3ab41d016c776bb29d9f5eff0cdb401d (diff)
Extend definition of inductives to include subtyping info
Diffstat (limited to 'kernel/univ.mli')
0 files changed, 0 insertions, 0 deletions