aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2014-01-25Adding a test for bug #3023.Pierre-Marie Pédrot
2014-01-15Test case containing a proof of false due to a DeBruijn off-by-one error in theMaxime Dénès
2014-01-13rename Paral-ITP demo fileEnrico Tassi
2014-01-13Paral-ITP demo: better commentsEnrico Tassi
2014-01-13STM: fix very simple demoEnrico Tassi
2014-01-10Fix bug#2080: error message on Ltac name clash with primitive tacticsxclerc
2014-01-06fix simple test for paral-itpEnrico Tassi
2014-01-06Add a test suite file for Ltac's "+" tactical.Arnaud Spiwack
2013-12-21Test case for the buggy commutative cut subterm rule.Maxime Dénès
2013-12-20micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...Frédéric Besson
2013-12-19test-suite/output/Notations : evar number changePierre Boutillier
2013-12-19Missing Fail in r16792Pierre Boutillier
2013-12-17test guard condition against feature incompatible with prop-extBruno Barras
2013-12-17Tentative fix of the guardedness checker by Christine and me. All stdlib and ...Matthieu Sozeau
2013-12-16Added test-suite for bug #2990.Pierre-Marie Pédrot
2013-12-12Better unification for [projT1] and [proj1_sig].Jason Gross
2013-12-06Remove duplicate test-suite file.Arnaud Spiwack
2013-12-06Fix the refine related test-suite files to account for the new refine.Arnaud Spiwack
2013-12-02Test case for bug#2848.xclerc
2013-12-02Test suite: update output reference.xclerc
2013-12-02Print logical name rather than path (thus allowing reproducible tests).xclerc
2013-11-29Testsuite: flatten the 'bugs/opened' directory.xclerc
2013-11-28Testsuite: remove the logic for 'bugs/opened/shouldnotsucceed' (unused)xclerc
2013-11-03test-suite fixuppboutill
2013-10-10Document: undoing inside a focused zone does not require unfocusinggareuselesinge
2013-10-10fake_ide: ported to Document + 2 tests for editing a proof (locally)gareuselesinge
2013-10-08Fixing 2 output test-suites.ppedrot
2013-10-07fake_ide: speak the new protocolgareuselesinge
2013-10-03Regression test suite for STMgareuselesinge
2013-10-01demo file for paral-itpgareuselesinge
2013-09-20Fix name clash in "failure/inductive.v".xclerc
2013-09-20Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.xclerc
2013-09-20Merge "inductive?.v" tests into a single "inductive.v" test.xclerc
2013-09-20Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.xclerc
2013-09-20Get rid of "shouldfail" subdirectory by moving tests to parent directory.xclerc
2013-09-20Wrong bug identifier.xclerc
2013-09-20Execute tests from the "bugs/closed" directory.xclerc
2013-09-20Update test for bug 2846 in order to use "Fail".xclerc
2013-09-20Use "Fail" rather than rely on exit code.xclerc
2013-09-19Uminus.v : prepare this test file for the use of Failletouzey
2013-09-19universes-buraliforti-redef.v : repair a match after Pierre B. syntax changesletouzey
2013-09-03Fixing some tests from the test-suite.ppedrot
2013-09-02* test-suite/success/Unicode_utf8:regisgia
2013-08-30Trickyer test for Paral-ITPgareuselesinge
2013-08-20Universe counters on slaves are in sync with mastergareuselesinge
2013-08-08Test for Paral-ITPgareuselesinge
2013-08-08Coqide ported to STMgareuselesinge
2013-08-08Fix testsuite so that it works with STMgareuselesinge
2013-08-04Added test for bug #2846.ppedrot
2013-08-04Added a test for bug #3062.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 19:32:24 +0000