aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/univnames.v
Commit message (Expand)AuthorAge
* Instances should obey universe binders even when defined by tactics.Gravatar Gaetan Gilbert2017-04-03
* Fix test suite after Matthieu's ed7af646f2e486b.Gravatar Maxime Dénès2015-10-28
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07