aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3825.v
AgeCommit message (Expand)Author
2016-05-03Fix bug #3825: Universe annotations on notations should pass through or be re...Pierre-Marie Pédrot