aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/2428.v
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2016-01-23 15:17:29 -0500
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2016-01-23 15:58:06 -0500
commit5cbcc8fd761df0779f6202fef935f07cfef8a228 (patch)
tree886d05ab59b157b812879facc6ef3fa3defc7d20 /test-suite/bugs/2428.v
parentccdc62a6b4722c38f2b37cbf21b14e5094255390 (diff)
Implement support for universe binder lists in Instance and Program Fixpoint/Definition.
Diffstat (limited to 'test-suite/bugs/2428.v')
0 files changed, 0 insertions, 0 deletions