aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3825.v
Commit message (Expand)AuthorAge
* Univs: allowing notations to take univ instancesGravatar Matthieu Sozeau2016-06-27
* Fix bug #3825: Universe annotations on notations should pass through or be re...Gravatar Pierre-Marie Pédrot2016-05-03