aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Fixing "clear" in internal_cut_replace: forbid dependencies in theGravatar Hugo Herbelin2014-06-13
* Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).Gravatar Hugo Herbelin2014-06-13
* Fix bug #3291, stack overflow in rewrite.Gravatar Matthieu Sozeau2014-06-11
* Fix bug #3289Gravatar Matthieu Sozeau2014-06-11
* Move bug # 3368 to closed bugsGravatar Matthieu Sozeau2014-06-11
* Add many more cases to the test-suiteGravatar Jason Gross2014-06-10
* Move closed bug 3314Gravatar Jason Gross2014-06-10
* Add a test-case for bug #3314 proving FalseGravatar Jason Gross2014-06-10
* Mark some progress in the HoTT/coq test-suiteGravatar Jason Gross2014-06-08
* Fix canonical structure resolution in unification (bug found in Ssreflect).Gravatar Matthieu Sozeau2014-06-08
* ind_tables: always declare side effects (Closes: HOTT#110)Gravatar Enrico Tassi2014-06-08
* - Better parsing and printing of named universes: Type{ident} and foo@{(ident...Gravatar Matthieu Sozeau2014-06-04
* - Force every universe level to be >= Prop, so one cannot "go under" it anymore.Gravatar Matthieu Sozeau2014-06-04
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* cbn understand ! Arguments directiveGravatar Pierre Boutillier2014-06-04
* A bug has been closed (HoTT/coq #105)Gravatar Jason Gross2014-06-03
* More on injection over a projectable "existT". - Fixing syntax "injection ......Gravatar Hugo Herbelin2014-05-31
* Fixing introduction patterns * and ** when used in a branch so that they do n...Gravatar Hugo Herbelin2014-05-31
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 09:31:39 +0000