aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Pos.compare_cont takes the comparison as first argumentGravatar Pierre Boutillier2014-02-28
| | | | Helps cbn tactic refolding
* test-suite: opaque term -> opaque proofGravatar Pierre Boutillier2014-02-28
|
* test-suite: New names for vars but the expected invariant is preservedGravatar Pierre Boutillier2014-02-28
|
* Fix output test-suite 'simpl tactic' -> 'reduction tactics'Gravatar Pierre Boutillier2014-02-28
|
* 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
| | | | code checking allowed sorts for elimination.
* 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 ↵Gravatar Frédéric Besson2013-12-20
| | | | and nia.
* 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
| | | | test-suite pass.
* 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
| | | | | | | This way, [fun A (P : A -> Prop) (X : sigT P) => proj1_sig X] unifies with [fun A (P : A -> Prop) (X : sigT P) => projT1 X]. This closes Bug 3043.
* Remove duplicate test-suite file.Gravatar Arnaud Spiwack2013-12-06
| | | | success/instantiate.v was a duplicate of bugs/closed/1041.v
* 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
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17046 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document: undoing inside a focused zone does not require unfocusingGravatar gareuselesinge2013-10-10
| | | | | | | | | | | | | To test this fake_ide has also been improved with the GOALS command. As for CoqIDE, ADDing a sentence does not force its evaluation. The "advance 1 sentence" button is an ADD + GOALS. If one of the ADDed sentences is wrong, GOALS receives the error. The GUI then backtracks to a safe state id (sent by Coq). fake_ide has GOALS (asserts that the goals call was OK) and FAILGOALS to assert it fails and backtrack to a valid state. see unfdo022.fake. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16873 85f007b7-540e-0410-9357-904b9bb8a0f7
* fake_ide: ported to Document + 2 tests for editing a proof (locally)Gravatar gareuselesinge2013-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16871 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing 2 output test-suites.Gravatar ppedrot2013-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16863 85f007b7-540e-0410-9357-904b9bb8a0f7
* fake_ide: speak the new protocolGravatar gareuselesinge2013-10-07
| | | | | | | | | A new syntax for .fake files, allowing multi line phrases and labeled script points (to go back to them). Test 7 fails because of a bug in STM (in a very spaghetti-like script). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16860 85f007b7-540e-0410-9357-904b9bb8a0f7
* Regression test suite for STMGravatar gareuselesinge2013-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16840 85f007b7-540e-0410-9357-904b9bb8a0f7
* demo file for paral-itpGravatar gareuselesinge2013-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16832 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix name clash in "failure/inductive.v".Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16800 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16799 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge "inductive?.v" tests into a single "inductive.v" test.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16798 85f007b7-540e-0410-9357-904b9bb8a0f7
* Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16797 85f007b7-540e-0410-9357-904b9bb8a0f7
* Get rid of "shouldfail" subdirectory by moving tests to parent directory.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16796 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wrong bug identifier.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Execute tests from the "bugs/closed" directory.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16794 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update test for bug 2846 in order to use "Fail".Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16793 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use "Fail" rather than rely on exit code.Gravatar xclerc2013-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16792 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uminus.v : prepare this test file for the use of FailGravatar letouzey2013-09-19
| | | | | | | | | | - Highlight the fact that the line defining "up" is the one which should fail. - Factor code with stdlib's Hurkens.v - This way, this test could become a "shouldnotfail" test by placing two final "Fail" (before the definitions of "up" and "paradox"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16791 85f007b7-540e-0410-9357-904b9bb8a0f7
* universes-buraliforti-redef.v : repair a match after Pierre B. syntax changesGravatar letouzey2013-09-19
| | | | | | | | | | This file, which is currently expected to fail at the last line (with Universe Inconsistency), was actually failing earlier after Pierre Boutillier changed the patterns (parameters are required now). A final "Fail" will soon arrives here to avoid such issue in the future... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16790 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing some tests from the test-suite.Gravatar ppedrot2013-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16760 85f007b7-540e-0410-9357-904b9bb8a0f7
* * test-suite/success/Unicode_utf8:Gravatar regisgia2013-09-02
| | | | | | Regression test for bug #3020. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16756 85f007b7-540e-0410-9357-904b9bb8a0f7
* Trickyer test for Paral-ITPGravatar gareuselesinge2013-08-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16740 85f007b7-540e-0410-9357-904b9bb8a0f7
* Universe counters on slaves are in sync with masterGravatar gareuselesinge2013-08-20
| | | | | | | | | | | | | | | Simple framework for remote counters. The slaves ask the master for a fresh value. On the master the thread manager answers with a bunch of fresh values (so that further requests can be immediately satisfied). Remote counters are guarded with a mutex on the master, because all slave managers as well as the master thread can access the counter at the same time. I know the name sucks. These counters are remote for the slaves, and local for the master. I'm open to suggestions... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16713 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 17:55:18 +0000