aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/1918.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-09Automatic introduction of names given before ":" in Lemma's andherbelin
Definition's is not so painless. It seems to however generally provide "nicer" scripts so let us keep it and update the contribs and test-suite accordingly. Also enforced that the actual introduced names to be exactly as given in the statements. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13097 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20Fixing bug #1918 (no occur-check in Meta unification was done yet!).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11818 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 21:11:13 +0000