aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/1322.v
AgeCommit message (Collapse)Author
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2017-10-15[stdlib] Fix warnings on deprecated `Add Setoid`Emilio Jesus Gallego Arias
The test suite cases are preserved until the feature is actually removed.
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
2007-12-21Ajouts de quelques tests sur les bugsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10400 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-16Correction du bug #1322notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10077 85f007b7-540e-0410-9357-904b9bb8a0f7