aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorArnaud Spiwack2014-09-23 11:11:08 +0200
committerArnaud Spiwack2014-09-24 12:25:55 +0200
commit4ca7900108f5b6d713b8d1c34afab284423bae65 (patch)
tree475639dcd46ac10143c0d9fb492e22502031b9b6 /kernel/nativecode.ml
parent926e25e8e9905e1ebbdbefc7ea3c8474cb523ec4 (diff)
Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions