aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
Commit message (Collapse)AuthorAge
* Add regression tests for univ. poly. and prim projGravatar Jason Gross2014-05-06
| | | | | | | | | | 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.
* Keep track of universes on coercion applications even if they're not ↵Gravatar Matthieu Sozeau2014-05-06
| | | | polymorphic (fixes bug #3043).
* Refresh some universes in cases.ml as they might appear in the term.Gravatar Matthieu Sozeau2014-05-06
|
* Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.Gravatar Matthieu Sozeau2014-05-06
|
* Retype application of fix_proto to get the right universes in ProgramGravatar Matthieu Sozeau2014-05-06
|
* Add regression tests for 3188 and 3265Gravatar Jason Gross2014-04-22
|
* Adding a test for bug #2923.Gravatar Pierre-Marie Pédrot2014-04-20
|
* Adding a test for bug #3285.Gravatar Pierre-Marie Pédrot2014-04-20
|
* better description of bug 3251Gravatar Enrico Tassi2014-04-10
|
* coqtop -batch refuses Back 1 but accepts Undo.Gravatar Pierre Boutillier2014-04-10
|
* By resolution of the CoqWG, instantiate must not be used now that refine worksGravatar Pierre Boutillier2014-04-10
|
* No more Coersion in Init.Gravatar Pierre Boutillier2014-04-10
|
* Define [projT3] and [proj3_sig]Gravatar Jason Gross2014-04-10
| | | | | | | | 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.
* Test case for bug 3037Gravatar Jason Gross2014-04-10
| | | | Closed in 4a8950ec7a0d9f2b216e67e69b446c064590a8e9
* Test case for 3164Gravatar Jason Gross2014-04-10
| | | | | | | Closed in 69c4d0fd7b8325187e8da697a9c283594047d. I used [Timeout 2] to distinguish between stack overflow and immediate return.
* Test case for bug 3262Gravatar Jason Gross2014-04-10
| | | | | | | Closed in f65fa9de8a4c9c12d933188a755b51508bd51921 I used [Timeout 2 Fail] to test the difference between immediate failure and stack overflow. Hopefully this is robust enough.
* Test case for bug #3217Gravatar Jason Gross2014-04-10
| | | | | | | 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.
* Add a regression test for bug 3001Gravatar Jason Gross2014-04-10
|
* Test for bug #3142, actually duplicate of #3262.Gravatar Hugo Herbelin2014-04-05
|
* Fixing bug #3228 (fixing precedence of ltac variables over variables in env).Gravatar Hugo Herbelin2014-04-05
|
* Add a test case for bug 3251Gravatar Jason Gross2014-04-02
| | | | It was closed in 5b39c3535f7b3383d89d7b844537244a4e7c0eca.
* Fixing bug #2900 (evar/evar unif was supposed to be treated inGravatar Hugo Herbelin2014-04-01
| | | | | | 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).
* Adding a test for bug #3023.Gravatar Pierre-Marie Pédrot2014-01-25
|
* Fix bug#2080: error message on Ltac name clash with primitive tacticsGravatar xclerc2014-01-10
|
* Missing Fail in r16792Gravatar Pierre Boutillier2013-12-19
|
* Added test-suite for bug #2990.Gravatar Pierre-Marie Pédrot2013-12-16
|
* Better unification for [projT1] and [proj1_sig].Gravatar Jason Gross2013-12-12
| | | | | | | 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.
* Fix the refine related test-suite files to account for the new refine.Gravatar Arnaud Spiwack2013-12-06
|
* Test case for bug#2848.Gravatar xclerc2013-12-02
|
* Testsuite: flatten the 'bugs/opened' directory.Gravatar xclerc2013-11-29
|
* Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16797 85f007b7-540e-0410-9357-904b9bb8a0f7
* Get rid of "shouldfail" subdirectory by moving tests to parent directory.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16796 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wrong bug identifier.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update test for bug 2846 in order to use "Fail".Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16793 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use "Fail" rather than rely on exit code.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16792 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added test for bug #2846.Gravatar ppedrot2013-08-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16663 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a test for bug #3062.Gravatar ppedrot2013-08-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16661 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a test for bug #3088.Gravatar ppedrot2013-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16650 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative fix for #3054: we refresh universes in a term generatedGravatar ppedrot2013-07-29
| | | | | | | 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
* Fixing bug #3093 by adding the asked test case.Gravatar ppedrot2013-07-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16634 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugfix: Fixing #3050Gravatar ppedrot2013-06-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection against "Bad recursive type" in w_unify0 (bug #3036).Gravatar herbelin2013-05-08
| | | | | | | | | | | | | | 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
* Added a unit test for bug #2230.Gravatar ppedrot2013-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finer fix for bug 3017, mark unresolvability only of goals that areGravatar msozeau2013-04-18
| | | | | | | 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
* Like in r16346, do not filter local definitions (here in theGravatar herbelin2013-04-17
| | | | | | | | | | | | | | 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
* Added regression test for bug #3023 which was solved by Matthieu'sGravatar herbelin2013-04-16
| | | | | | | 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
* Equality: avoid some unprotected List.nth (fix #2837)Gravatar letouzey2013-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16392 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enrich test-suite with a test for #3022.Gravatar ppedrot2013-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16390 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enrich test-suite with a test for #2928Gravatar letouzey2013-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enrich test-suite with a test for #2734Gravatar letouzey2013-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16365 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 20:02:25 +0000