aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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
* Test suite: update output reference.Gravatar xclerc2013-12-02
* Print logical name rather than path (thus allowing reproducible tests).Gravatar xclerc2013-12-02
* Testsuite: flatten the 'bugs/opened' directory.Gravatar xclerc2013-11-29
* Testsuite: remove the logic for 'bugs/opened/shouldnotsucceed' (unused)Gravatar xclerc2013-11-28
* test-suite fixupGravatar pboutill2013-11-03
* Document: undoing inside a focused zone does not require unfocusingGravatar gareuselesinge2013-10-10
* fake_ide: ported to Document + 2 tests for editing a proof (locally)Gravatar gareuselesinge2013-10-10
* Fixing 2 output test-suites.Gravatar ppedrot2013-10-08
* fake_ide: speak the new protocolGravatar gareuselesinge2013-10-07
* Regression test suite for STMGravatar gareuselesinge2013-10-03
* demo file for paral-itpGravatar gareuselesinge2013-10-01
* Fix name clash in "failure/inductive.v".Gravatar xclerc2013-09-20
* Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.Gravatar xclerc2013-09-20
* Merge "inductive?.v" tests into a single "inductive.v" test.Gravatar xclerc2013-09-20
* 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
* Execute tests from the "bugs/closed" directory.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
* Uminus.v : prepare this test file for the use of FailGravatar letouzey2013-09-19
* universes-buraliforti-redef.v : repair a match after Pierre B. syntax changesGravatar letouzey2013-09-19
* Fixing some tests from the test-suite.Gravatar ppedrot2013-09-03
* * test-suite/success/Unicode_utf8:Gravatar regisgia2013-09-02
* Trickyer test for Paral-ITPGravatar gareuselesinge2013-08-30
* Universe counters on slaves are in sync with masterGravatar gareuselesinge2013-08-20
* Test for Paral-ITPGravatar gareuselesinge2013-08-08
* Coqide ported to STMGravatar gareuselesinge2013-08-08
* Fix testsuite so that it works with STMGravatar gareuselesinge2013-08-08
* Added test for bug #2846.Gravatar ppedrot2013-08-04