aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
AgeCommit message (Collapse)Author
2014-05-06Keep track of universes on coercion applications even if they're not ↵Matthieu Sozeau
polymorphic (fixes bug #3043).
2014-05-06Refresh some universes in cases.ml as they might appear in the term.Matthieu Sozeau
2014-05-06Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.Matthieu Sozeau
2014-05-06Retype application of fix_proto to get the right universes in ProgramMatthieu Sozeau
2014-04-22Add regression tests for 3188 and 3265Jason Gross
2014-04-20Adding a test for bug #2923.Pierre-Marie Pédrot
2014-04-20Adding a test for bug #3285.Pierre-Marie Pédrot
2014-04-10better description of bug 3251Enrico Tassi
2014-04-10coqtop -batch refuses Back 1 but accepts Undo.Pierre Boutillier
2014-04-10By resolution of the CoqWG, instantiate must not be used now that refine worksPierre Boutillier
2014-04-10No more Coersion in Init.Pierre Boutillier
2014-04-10Define [projT3] and [proj3_sig]Jason Gross
Also allow [projT1]/[projT2] to work for [sigT2]s and [proj1_sig]/[proj2_sig] to work for [sig2]s, by means of coercions. This closes Bug 3044. This closes Pull Request #4.
2014-04-10Test case for bug 3037Jason Gross
Closed in 4a8950ec7a0d9f2b216e67e69b446c064590a8e9
2014-04-10Test case for 3164Jason Gross
Closed in 69c4d0fd7b8325187e8da697a9c283594047d. I used [Timeout 2] to distinguish between stack overflow and immediate return.
2014-04-10Test case for bug 3262Jason Gross
Closed in f65fa9de8a4c9c12d933188a755b51508bd51921 I used [Timeout 2 Fail] to test the difference between immediate failure and stack overflow. Hopefully this is robust enough.
2014-04-10Test case for bug #3217Jason Gross
It was fixed in c3feef4ed5dec126f1144dec91eee9c0f0522a94. The test case uses [Timeout 2] to test for "Coq runs instantaneously rather than running out of memory". Hopefully this is robust enough.
2014-04-10Add a regression test for bug 3001Jason Gross
2014-04-05Test for bug #3142, actually duplicate of #3262.Hugo Herbelin
2014-04-05Fixing bug #3228 (fixing precedence of ltac variables over variables in env).Hugo Herbelin
2014-04-02Add a test case for bug 3251Jason Gross
It was closed in 5b39c3535f7b3383d89d7b844537244a4e7c0eca.
2014-04-01Fixing bug #2900 (evar/evar unif was supposed to be treated inHugo Herbelin
solve_simple_eqn but in case the second evar was hidden behind a local variable, it arrived in evar_define and imitate, wrongly assuming progress).
2014-01-25Adding a test for bug #3023.Pierre-Marie Pédrot
2014-01-10Fix bug#2080: error message on Ltac name clash with primitive tacticsxclerc
2013-12-16Added test-suite for bug #2990.Pierre-Marie Pédrot
2013-12-12Better unification for [projT1] and [proj1_sig].Jason Gross
This way, [fun A (P : A -> Prop) (X : sigT P) => proj1_sig X] unifies with [fun A (P : A -> Prop) (X : sigT P) => projT1 X]. This closes Bug 3043.
2013-12-06Fix the refine related test-suite files to account for the new refine.Arnaud Spiwack
2013-12-02Test case for bug#2848.xclerc
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
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-20Wrong bug identifier.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16795 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
2013-08-04Added a test for bug #3062.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16661 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-01Added a test for bug #3088.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16650 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-29Tentative fix for #3054: we refresh universes in a term generatedppedrot
by congruence, as it seems to be done methodically on the remaining of this plugin. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16642 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-25Fixing bug #3093 by adding the asked test case.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16634 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-27Bugfix: Fixing #3050ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16608 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-08Protection against "Bad recursive type" in w_unify0 (bug #3036).herbelin
Morally, unification wants to unify "fun x:Meta => Meta" with "fun x:nat => match x with ... end". Retyping is asked to type "match x with ... end" in the context "x:Meta" where the type of x has de facto been lost. Retyping fails. I don't see an easy remedy since w_unify0 builds the unifier lazily, and I'm not sure it is worth to propagate the unifier to retyping so that it knows it. After all, the call to retyping in w_unify0 is not so critical. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16489 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-27Added a unit test for bug #2230.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16460 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-18Finer fix for bug 3017, mark unresolvability only of goals that aremsozeau
instances of metas in clenvtac. Makes Math-Classes compile again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16429 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Like in r16346, do not filter local definitions (here in theherbelin
type-based second-order unification algorithm). In type-based second-order unification algorithm, protect local definitions in instances of evars to wrongly be considered as potentially flexible. Altogether, this fixes the anomaly in #3003 (even if some additional work has to be done to improve the resulting error message, see next commit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16414 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-16Added regression test for bug #3023 which was solved by Matthieu'sherbelin
commit r16134 (eta was missing in Flexible/Rigid and SemiFlexible/Rigid conversion problems). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16409 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-10Equality: avoid some unprotected List.nth (fix #2837)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16392 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-08Enrich test-suite with a test for #3022.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16390 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Enrich test-suite with a test for #2928letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16367 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Enrich test-suite with a test for #2734letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16365 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25Add the test-case of bug 2750 in the test-suiteletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16362 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Robust display of NotConvertibleTypeField errors (fix #3008, #2995)letouzey
Since the nametab isn't aware of everything needed to print mismatched types (cf the bug test-cases), we create a robust term printer that known how to print a fully-qualified name when [shortest_qualid_of_global] has failed. These Printer.safe_pr_constr and alii are meant to never fail (at worse they display "??", for instance when the env isn't rich enough). Moreover, the environnement may have changed between the raise of NotConvertibleTypeField and its display, so we store the original env in the exception. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16342 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Firstorder: record with defined field aren't conjonctions (fix #2629)letouzey
The let-in in the type of constructor was perturbating the Hipattern.dependent check, leading firstorder to consider too much inductives as dependent-free conjonctions, ending with lift errors (UNBOUND_REL_-2, ouch). This patch is probably overly cautious : if the variable of the let-in is used, we consider the constructor to be dependent. If someday somebody feels it necessary, he/she could try to reduce the let-in's instead... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16339 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-29 04:29:24 +0000