aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/vm_univ_poly.v
AgeCommit message (Collapse)Author
2016-06-27Forbidding silently dropped universes instances inMatthieu Sozeau
internalization. Patch by PMP, test-suite fix by MS.
2015-12-09bug fixes to vm computation + test cases.Gregory Malecha