aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3043.v
AgeCommit message (Expand)Author
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2014-05-08Fixing test-suite for bug #3043.Pierre-Marie Pédrot
2014-05-06Keep track of universes on coercion applications even if they're not polymorp...Matthieu Sozeau
2014-04-10No more Coersion in Init.Pierre Boutillier
2013-12-12Better unification for [projT1] and [proj1_sig].Jason Gross