aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
Commit message (Expand)AuthorAge
* Add regression tests for univ. poly. and prim projGravatar Jason Gross2014-05-06
* Keep track of universes on coercion applications even if they're not polymorp...Gravatar Matthieu Sozeau2014-05-06
* 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
* Test case for bug 3037Gravatar Jason Gross2014-04-10
* Test case for 3164Gravatar Jason Gross2014-04-10
* Test case for bug 3262Gravatar Jason Gross2014-04-10
* Test case for bug #3217Gravatar Jason Gross2014-04-10
* 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
* Fixing bug #2900 (evar/evar unif was supposed to be treated inGravatar Hugo Herbelin2014-04-01
* 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
* 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
* Get rid of "shouldfail" subdirectory by moving tests to parent directory.Gravatar xclerc2013-09-20
* Wrong bug identifier.Gravatar xclerc2013-09-20
* Update test for bug 2846 in order to use "Fail".Gravatar xclerc2013-09-20
* Use "Fail" rather than rely on exit code.Gravatar xclerc2013-09-20
* Added test for bug #2846.Gravatar ppedrot2013-08-04
* Added a test for bug #3062.Gravatar ppedrot2013-08-04
* Added a test for bug #3088.Gravatar ppedrot2013-08-01
* Tentative fix for #3054: we refresh universes in a term generatedGravatar ppedrot2013-07-29
* Fixing bug #3093 by adding the asked test case.Gravatar ppedrot2013-07-25
* Bugfix: Fixing #3050Gravatar ppedrot2013-06-27
* Protection against "Bad recursive type" in w_unify0 (bug #3036).Gravatar herbelin2013-05-08
* Added a unit test for bug #2230.Gravatar ppedrot2013-04-27
* Finer fix for bug 3017, mark unresolvability only of goals that areGravatar msozeau2013-04-18
* Like in r16346, do not filter local definitions (here in theGravatar herbelin2013-04-17
* Added regression test for bug #3023 which was solved by Matthieu'sGravatar herbelin2013-04-16
* Equality: avoid some unprotected List.nth (fix #2837)Gravatar letouzey2013-04-10
* Enrich test-suite with a test for #3022.Gravatar ppedrot2013-04-08
* Enrich test-suite with a test for #2928Gravatar letouzey2013-03-25
* Enrich test-suite with a test for #2734Gravatar letouzey2013-03-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 23:26:09 +0000