aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened
AgeCommit message (Collapse)Author
2014-06-08ind_tables: always declare side effects (Closes: HOTT#110)Enrico Tassi
declare takes care of ignoring side effects that are available in the global environment. This is yet another instance of what the "abominion" (aka abstract) can do: the code was checking for the existence in the environment of the elimination principle, and not regenerating it (nor declaring the corresponding side effect) if the elimination principle is used twice. Of course to functionalize the imperative actions on the environment when two proofs generated by abstract use the same elim principle, such elim principle has to be inlined twice, once in each abstracted proof. In other words, a side effect generated by a tactic inside an abstract is *global* but will be made local, si it must always be declared, no matter what. Now the system works like this: - side effects are always declared, even if a caching mechanism thinks the constant is already there (it can be there, no need to regenerate it but the intent to generate it *must* be declared anyhow) - at Qed time, we filter the list of side effects and decide which ones are really needed to be inlined. bottom line: STOP using abstract.
2014-06-03A bug has been closed (HoTT/coq #105)Jason Gross
2014-05-16Fix unification of non-unfoldable primitive projections in evarconv.Matthieu Sozeau
2014-05-12Update various polyproj bugs w.r.t. latest trunkJason Gross
2014-05-10Add appropriate Fail(s) to opened bugsJason Gross
The contract is that a file in bugs/opened should not raise errors if the bug is still open. Some of them fail for different reasons than they used to; I'm not sure what to do about these.
2014-05-10Move opened bugs to bugs/openedJason Gross
2014-05-09Refresh universes for Ltac's type_of, as the term can be used anywhere,Matthieu Sozeau
fixing two opened bugs from HoTT/coq.
2014-05-06Add regression tests for univ. poly. and prim projJason Gross
These regression tests are aggregated from the various bugs I (and others) have reported on https://github.com/HoTT/coq/issues relating to universe polymorphism, primitive projections, and eta for records. These are the tests that trunk currently passes. I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the number of the issue in GitHub), but I couldn't think of a better one.
2013-12-19Missing Fail in r16792Pierre Boutillier
2013-11-29Testsuite: flatten the 'bugs/opened' directory.xclerc
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-01-18Unset Asymmetric Patternspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18r14204 and 14218 continued: completely removing test for bug #2490,herbelin
leaving the decision of what to do with it to Matthieu; sorry for the confusion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14219 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-18Partial backtrack on wrong r14204: bug #2490 still open.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14218 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"herbelin
by a regular error in v8.3. Example behaves better in trunk thanks to new proof engine. In fact, there are two distinct solutions to a unification problem: should "refine" commit to one of them or leave the problem open? For trunk, improved the unification error message by enforcing nf_evar (but at some time, nf_evar in error messages should move to himsg because it is costly when errors are used for backtracking). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13127 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-07Granting wish #2251 thanks to commit 12900 solved bug 1416.v (whichherbelin
was actually failing for another reason than the reason originally filled in the bug tracker) and revealed a bug in the unification.v test file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12906 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-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-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-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-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-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-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 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
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-11Test pour le bug #1754notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10364 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-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 #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-02-27 22:41:37 +0000