aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Adding test-suite for bug #3355.Gravatar Pierre-Marie Pédrot2014-05-30
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* Fix unification of non-unfoldable primitive projections in evarconv.Gravatar Matthieu Sozeau2014-05-16
* Test-suite for bug #3259.Gravatar Pierre-Marie Pédrot2014-05-13
* Update various polyproj bugs w.r.t. latest trunkGravatar Jason Gross2014-05-12
* Add appropriate Fail(s) to opened bugsGravatar Jason Gross2014-05-10
* Move opened bugs to bugs/openedGravatar Jason Gross2014-05-10
* Add more regression tests for univ poly/prim projGravatar Jason Gross2014-05-10
* Refresh universes for Ltac's type_of, as the term can be used anywhere,Gravatar Matthieu Sozeau2014-05-09
* Merge branch 'working-polyproj-tests' of https://github.com/JasonGross/coq in...Gravatar Matthieu Sozeau2014-05-09
|\
* | Fix second-order matching to properly check that the predicate found byGravatar Matthieu Sozeau2014-05-09
* | Simplification and improvement of "subst x" in such a way that itGravatar Hugo Herbelin2014-05-08
* | Fixing test-suite for bug #3043.Gravatar Pierre-Marie Pédrot2014-05-08
* | Fixing output test-suite: since universe polymorphism, the Print commandGravatar Pierre-Marie Pédrot2014-05-08
* | Adding test-suite for bug #3242.Gravatar Pierre-Marie Pédrot2014-05-06
| * 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
* Comment in Funind.v test-suite fileGravatar 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
* - Fix arity handling in retyping (de Bruijn bug!)Gravatar Matthieu Sozeau2014-05-06
* Fix restrict_universe_context removing some universes that do appear in the t...Gravatar Matthieu Sozeau2014-05-06
* Fix declarations of monomorphic assumptionsGravatar Matthieu Sozeau2014-05-06
* - Fix RecTutorial, and mutual induction schemes getting the wrong names.Gravatar Matthieu Sozeau2014-05-06
* - Fixes for canonical structure resolution (check that the initial term indee...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Update test-suite Makefile to handle coq-prog-argsGravatar Jason Gross2014-05-02
* Fixing #3293 (eta-expansion at "match" printing time was failingGravatar Hugo Herbelin2014-04-28
* 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
* Add another critical bug to the test-suite.Gravatar Maxime Dénès2014-04-09
* Adapt test-suite to -I is ML onlyGravatar Pierre Boutillier2014-04-09
* 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
* Remove option -g as it is non-portable yet does not have any effect on the te...Gravatar Guillaume Melquiond2014-04-04
* 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
* test for apply + TC resolutionGravatar Enrico Tassi2014-03-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 16:32:17 +0000