aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldfail
AgeCommit message (Collapse)Author
2013-09-20Get rid of "shouldfail" subdirectory by moving tests to parent directory.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16796 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Update test for bug 2846 in order to use "Fail".xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16793 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Use "Fail" rather than rely on exit code.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16792 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-04Added test for bug #2846.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16663 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-18Fix bug #2586 and enhance clsubst* as well as a side effectmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14570 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-21Some fixes of the test-suite scriptsletouzey
In particular, the Fail meta-command cannot for the moment catch a Syntax Error, which is raised by Vernac.parse_sentence, before we even now that the line starts by a Fail... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13847 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-05Granting wish #2251 (forbidding rewriting a term reduced to an evar)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12900 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
2008-11-26closed bug 1898: fold x in x; added a reordering primitive tacticbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11632 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-23Fixed bug #2006 (type constraint on Record was not taken into account) +herbelin
slight improving of the printing of record. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11619 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-25A better test for relations being setoids or not: do leibniz rewrite iffmsozeau
the applied relation is an abbreviation for @eq. Fixes bug #1915. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11264 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-21- Fixing bug 1703 ("intros until n" falls back on the variable name whenherbelin
the latter is bound to a var which is not a quantified one - this led to remove a line marked "temporary compatibility" ... ; made a distinction between quantified hypothesis as for "intros until" and binding names as in "apply with"; in both cases, we now expect that a identifier not used as a variable, as in "apply f_equal with f:=g" where "f" is a true binder name in f_equal, must not be used as a variable elsewhere [see corresponding change in Ints/Tactic.v]) - Fixing bug 1643 (bug in the algorithm used to possibly reuse a global name in the recursive calls of a coinductive term) - Fixing bug 1699 (bug in contracting nested patterns at printing time when the return clause of the subpatterns is dependent) - Fixing bug 1697 (bug in the TacAssert clause of Tacinterp.subst_tactic) - Fixing bug 1678 (bug in converting constr_pattern to constr in Constrextern) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10131 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 04:04:55 +0000