aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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
* nanoPG: better copy/pasteGravatar Enrico Tassi2014-03-13
* Never suppress the typing constraint of bound variables whose name wasGravatar Pierre-Marie Pédrot2014-03-01
* Pos.compare_cont takes the comparison as first argumentGravatar Pierre Boutillier2014-02-28
* test-suite: opaque term -> opaque proofGravatar Pierre Boutillier2014-02-28
* test-suite: New names for vars but the expected invariant is preservedGravatar Pierre Boutillier2014-02-28
* Fix output test-suite 'simpl tactic' -> 'reduction tactics'Gravatar Pierre Boutillier2014-02-28
* fake_ide: ported to spawnGravatar Enrico Tassi2014-02-10
* Adding a test for bug #3023.Gravatar Pierre-Marie Pédrot2014-01-25
* Test case containing a proof of false due to a DeBruijn off-by-one error in theGravatar Maxime Dénès2014-01-15
* rename Paral-ITP demo fileGravatar Enrico Tassi2014-01-13
* Paral-ITP demo: better commentsGravatar Enrico Tassi2014-01-13
* STM: fix very simple demoGravatar Enrico Tassi2014-01-13
* Fix bug#2080: error message on Ltac name clash with primitive tacticsGravatar xclerc2014-01-10
* fix simple test for paral-itpGravatar Enrico Tassi2014-01-06
* Add a test suite file for Ltac's "+" tactical.Gravatar Arnaud Spiwack2014-01-06
* Test case for the buggy commutative cut subterm rule.Gravatar Maxime Dénès2013-12-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 11:23:57 +0000