aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/335.v
AgeCommit message (Collapse)Author
2017-10-23Move bug files to match their new GitHub ID (fixes #6001).Théo Zimmermann
2015-01-18Revert "Fix files in test-suite having to do with Require inside modules."Maxime Dénès
This reverts commit a7ed77403cd15ba1cc2c05f2b6193b46f0028eda.
2015-01-12Fix files in test-suite having to do with Require inside modules.Maxime Dénès
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