aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3922.v
Commit message (Expand)AuthorAge
* Fix bug #3825: Universe annotations on notations should pass through or be re...Gravatar Pierre-Marie Pédrot2016-05-03
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Fix bug #4254 with the help of J.H. JourdanGravatar Matthieu Sozeau2015-06-26
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Test for bug #3922.Gravatar Pierre-Marie Pédrot2015-02-16