aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
2013-08-01Added a test for bug #3088.ppedrot
2013-07-29Tentative fix for #3054: we refresh universes in a term generatedppedrot
2013-07-29better error message for unexpected renaming (closes #2987)gareuselesinge
2013-07-25Fixing bug #3093 by adding the asked test case.ppedrot
2013-07-17More dynamic argument scopesletouzey
2013-07-10Continuing r16621 on injection intro-patterns:herbelin
2013-07-09Revising r16550 about providing intro patterns for applying injection:herbelin
2013-06-27Bugfix: Fixing #3050ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 14:59:01 +0000