aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3392.v
AgeCommit message (Expand)Author
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-02-27Made test for #3392 rely less on unification.Maxime Dénès
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2014-06-263392 is now closed thanks to E. Tassi.Matthieu Sozeau