aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3922.v
AgeCommit message (Expand)Author
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2016-05-03Fix bug #3825: Universe annotations on notations should pass through or be re...Pierre-Marie Pédrot
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-06-26Fix bug #4254 with the help of J.H. JourdanMatthieu Sozeau
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-02-16Test for bug #3922.Pierre-Marie Pédrot