aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2014-03-26test for apply + TC resolutionEnrico Tassi
2014-03-13nanoPG: better copy/pasteEnrico Tassi
2014-03-01Never suppress the typing constraint of bound variables whose name wasPierre-Marie Pédrot
2014-02-28Pos.compare_cont takes the comparison as first argumentPierre Boutillier
2014-02-28test-suite: opaque term -> opaque proofPierre Boutillier
2014-02-28test-suite: New names for vars but the expected invariant is preservedPierre Boutillier
2014-02-28Fix output test-suite 'simpl tactic' -> 'reduction tactics'Pierre Boutillier
2014-02-10fake_ide: ported to spawnEnrico Tassi
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 18:40:27 +0000