aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/2262.v
AgeCommit message (Collapse)Author
2013-09-20Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16797 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Fix bug #2262: bad implicit argument number by avoiding countingmsozeau
products as implicit if they're part of a term and not a type (issue a warning instead). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13101 85f007b7-540e-0410-9357-904b9bb8a0f7