aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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
* Added a test for bug #3062.Gravatar ppedrot2013-08-04
* Added a test for bug #3088.Gravatar ppedrot2013-08-01
* Tentative fix for #3054: we refresh universes in a term generatedGravatar ppedrot2013-07-29
* better error message for unexpected renaming (closes #2987)Gravatar gareuselesinge2013-07-29
* Fixing bug #3093 by adding the asked test case.Gravatar ppedrot2013-07-25
* More dynamic argument scopesGravatar letouzey2013-07-17
* Continuing r16621 on injection intro-patterns:Gravatar herbelin2013-07-10
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
* Bugfix: Fixing #3050Gravatar ppedrot2013-06-27
* Fix [setoid_rewrite] forgetting some evars that are produced when typecheckin...Gravatar msozeau2013-06-10
* Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as anGravatar herbelin2013-06-02
* Fixing a regression in unification introduced in r16205 (error raisedGravatar herbelin2013-05-14
* Updating some output tests in test-suite:Gravatar herbelin2013-05-09
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* Protection against "Bad recursive type" in w_unify0 (bug #3036).Gravatar herbelin2013-05-08
* Declaration of multiple hypotheses or parameters now share typingGravatar herbelin2013-05-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 15:42:13 +0000