aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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
* micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...Gravatar Frédéric Besson2013-12-20
* test-suite/output/Notations : evar number changeGravatar Pierre Boutillier2013-12-19
* Missing Fail in r16792Gravatar Pierre Boutillier2013-12-19
* test guard condition against feature incompatible with prop-extGravatar Bruno Barras2013-12-17
* Tentative fix of the guardedness checker by Christine and me. All stdlib and ...Gravatar Matthieu Sozeau2013-12-17
* 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
* Remove duplicate test-suite file.Gravatar Arnaud Spiwack2013-12-06
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 16:18:24 +0000