aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytecodes.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-10-28 11:02:09 -0400
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-10-28 11:02:52 -0400
commitb5a0e384b405f64fd0854d5e88b55e8c2a159c02 (patch)
tree6f5ae6fc34acb395543c91dfd3e172d30998be7c /kernel/cbytecodes.ml
parente3ec13976d39909ac6f1a82bf1b243ba8a895190 (diff)
Univs: fix bug #4375, accept universe binders on (co)-fixpoints
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions