aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/univnames.v
AgeCommit message (Expand)Author
2017-04-03Instances should obey universe binders even when defined by tactics.Gaetan Gilbert
2015-10-28Fix test suite after Matthieu's ed7af646f2e486b.Maxime Dénès
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau