aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3513.v
Commit message (Expand)AuthorAge
* Change Implicit Arguments to Arguments in test-suiteGravatar Jasper Hugunin2018-03-30
* Remove deprecated options related to typeclasses.Gravatar Théo Zimmermann2018-03-04
* Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
* Revert part of a477dc, disallow_shelvedGravatar Matthieu Sozeau2016-11-15
* Fix handling of only_classes at toplevelGravatar Matthieu Sozeau2016-11-03
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Fix bug #3732: firstorder was using detyping to build existentialGravatar Matthieu Sozeau2015-03-03