aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2008-09-03Fix bug #1935, reworking the reflexivity, symmetry... tactics to usemsozeau
the same typeclass method application tactic that's available to users. Modify a bit the _red tactics to accomodate the new setup and comment some dead code in setoid_replace. Next step is removing it completely. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11355 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
2008-07-22Add test-suite file for bug# 1905 and minor fix in Program/Equality.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11245 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
majuscule - si pas un ident ou un terme - et se terminent par un point). Restent quelques utilisations de "error" qui sont liées à des usages internes, ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-03Prise en compte de changments dans subtacnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11203 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-10- Correct handling of DependentMorphism error, using tclFAIL instead ofmsozeau
letting the exception go uncatched. - Reorder definitions in Morphisms, move the PER on (R ==> R') in Morphisms where it can be declared properly. Add an instance for Equivalence => Per. - Change bug#1604 test file to the new semantics of [setoid_rewrite at] - More unicode characters parsed by coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11092 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-09- Documentation de admit et Print Assumptions.herbelin
- Relecture, mise à jour, correction d'erreurs et petite réorganisation du chapitre sur les commandes vernaculaires. - Correction bug #1865 (rafraichissement des univers algébriques). - Suppression de la dépendance du initial.coq en les noms longs des fichiers de façons à ce que les dépendances ne soient que purement logique. - Encore un (petit) bug undo ide. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11077 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-03Temporarily disabling automatic test for bug 1338.vnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11041 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-29fixed bug #1780: a lift was missing (match predicate)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11017 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-07Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757herbelin
+ un error qui devrait être un anomaly git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10893 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-28Backtrack on using metas eagerly in auto, only done in "new auto" formsozeau
now. Fix proof scripts that failed correspondingly. Should make many contribs compile again... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10863 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-25- Fix bug in eterm which was not taking filtered contexts in evars intomsozeau
account. - Add test case for bug #1844 on Combined Scheme. - Change Reflexive_partial_app_morphism to require a Reflexive proof to cut down search earlier, without losing anything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10846 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-21- Correct unification for the rewrite variant of setoid_rewrite,msozeau
so that the example of bug #1425 is accepted. - Backtrack level of notations for morphism signatures to 55. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10825 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-21- Parameterize unification by two sets of transparent_state, one for openmsozeau
term unification (for constant and variable delta unfolding) and one to parameterize closed-term conversion. Most of the time conversion uses full delta and unification does no delta. This fine-grain is used in rewrite/setoid_rewrite, where only closed-term delta on global constants is allowed. - Interpret Hint Unfold as a directive for delta conversion in auto/eauto when applying lemmas (i.e., for Resolve and Immediate hints). - Remove ad-hoc support for this in typeclasses. Now setoid_rewrite works correctly w.r.t. the old version regarding local definitions. - Fix closed bugs which needed updating due to syntax modifications. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10824 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-17Bug squashing day !msozeau
- Closed bugs 121, 1696, 1438, 1425, 1696, 1604, 1738, 1760, 1683 related to setoids. Add corresponding test files. - Add new modulo_zeta flag to control zeta during unification (e.g. not allowed for setoid_rewrite unification, but ok for almost everything else). - Various fixes in class_tactics with respect to evars and error messages. - Correct error message for NoOccurenceFound, distinguishing between a rewrite in the goal or an hypothesis. - Move notations for ==>, --> and ++> to level 90 as suggested by Russell O'Conor. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10813 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-15Mises à jour bugs, CHANGES, code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10801 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-29Fix test-suite files, change conflicting notation "->rel" and the othersmsozeau
to "-R>" and the like. Split more precisely in inference of case predicate between the new code which currently works only for matched variables and the old one which works better on variables appearing in matched terms types (the two could also be merged). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10729 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-28Correction du bug 1816 (ajout d'un lemme dans Znat) et suppressionnotin
d'un test non significatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10726 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-26Diverses petites modifs dans la test-suite:notin
test-suite/output/ZSyntax.out typo test-suite/bugs/closed/shouldsucceed/1776.v bug closed test-suite/success/extraction.v test-suite/success/extraction.v test-suite/bugs/closed/shouldsucceed/846.v backtrack sur le commit 10639 test-suite/bugs/closed/shouldsucceed/1322.v: petites modifications suite aux changement de setoid_replace test-suite/bugs/closed/shouldsucceed/1414.v: petites modifications suite aux changement dans Program git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10723 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-17Add the possibility of specifying constants to unfold for typeclassmsozeau
resolution. Add [relation] and Setoid's [equiv] as such objects. Considerably simplify resolve_all_evars for typeclass resolution, adding a further refinement (and hack): evars get classified as non-resolvable (using the evar_extra dynamic field) if they are turned into a goal. This makes it possible to perform nested typeclass resolution without looping. We take advantage of that in Classes/Morphisms where [subrelation_tac] is added to the [Morphism] search procedure and calls the apply tactic which itself triggers typeclass resolution. Having [subrelation_tac] as a tactic instead of an instance, we can actually force that it is applied only once in each search branch and avoid looping. We could get rid of the hack when we have real goals-as-evars functionality (hint hint). Also fix some test-suite scripts which were still calling [refl] instead of [reflexivity]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10687 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-16Misc: Add test for bug 1704, now closed. Add usual syntax for lists inmsozeau
Program.Syntax along with stronger implicits. Update dependent induction test file using unicode syntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10682 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-08Fix bugs that were reopened due to the change of setoidmsozeau
implementation. Mostly syntax changes when declaring parametric relations, but also some declarations were relying on "default" relations on some carrier. Added a new DefaultRelation type class that allows to do that, falling back to the last declared Equivalence relation by default. This will be bound to Add Relation in the next commit. Also, move the "left" and "right" notations in Program.Utils to "in_left" and "in_right" to avoid clashes with existing scripts. Minor change to record to allow choosing the name of the argument for the record in projections to avoid possible incompatibilities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10639 85f007b7-540e-0410-9357-904b9bb8a0f7
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-03-02 13:51:52 +0000