aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2008-02-08Backport code from command.ml to subtac_command.ml for defininingmsozeau
recursive definitions. Now program accepts cofixpoints and uses the new way infer structurally decreasing arguments. Also, checks for correct recursive calls before giving the definition to the obligations machine (solves part 1 of bug #1784). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10529 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-05Ajout d'un test pour le bug #1787notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10507 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-01Ajout de 2 testsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10499 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-24Fermeture du bug #1754notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10472 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-23Ajout d'un test pour le bug #1779notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10468 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-23Ajout d'un test pour le mode déclaratif + test pour le bug #1776notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10466 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-21Correction du bug #1754notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10458 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-02Better resolution of implicit parameters in typeclass binders, add ↵msozeau
extensionality tactic to apply the axiom properly and fix test-suite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10415 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-12-12Ajout d'un test pour le bug #1100notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10370 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-11Test pour le bug #1754notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10364 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-04Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10172 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-21Correction d'un bug dans check + ajout de testsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10134 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
2007-08-22Correction du bug #1634 + ajout de bugs dans la test-suitenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10085 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
2007-08-16Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;notin
modification de interp_ltac_reference pour passer les ids utilisées dans le contexte d'appel d'une tactique. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10076 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-10Modification de la test suite pour intégrer des tests spécifiques auxnotin
bugs soumis sur Coq-bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10068 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-21 15:18:13 +0000