aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/Makefile
Commit message (Expand)AuthorAge
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2016-07-04
|\
| * test-suite: test checking of libraries checksum.Gravatar Maxime Dénès2016-07-04
* | fix test-suite/ide Makefile (stupid typo)Gravatar Enrico Tassi2016-06-15
* | test-suiet: run fake_id as before pr/173 was mergedGravatar Enrico Tassi2016-06-14
* | STM: code cleanupGravatar Enrico Tassi2016-05-10
* | Do that "make" in test-suite writes failures as a default togetherGravatar Hugo Herbelin2016-04-19
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\|
| * Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\|
| * Adding a target report to test-suite's Makefile to get a short summary.Gravatar Hugo Herbelin2015-12-02
* | New algorithm for universe cycle detections.Gravatar Jacques-Henri Jourdan2015-12-01
|/
* Univs: the stdlib now needs 5 universesGravatar Matthieu Sozeau2015-10-02
* Updating the documentation and the toolchain w.r.t. the change in -compile.Gravatar Pierre-Marie Pédrot2015-09-25
* test-suite: Fix test-suite MakefileGravatar Matthieu Sozeau2015-07-07
* Flag -test-mode intended to be used for ad-hoc prints in test-suiteGravatar Enrico Tassi2015-05-29
* camlp4: grep away warnings in output/* testsGravatar Enrico Tassi2015-03-30
* There was one more universe needed due to the use of now non-universe-polymor...Gravatar Matthieu Sozeau2015-01-18
* Back to 4 expected universes.Gravatar Matthieu Sozeau2015-01-17
* STM: fix handling of side effects in vio2voGravatar Enrico Tassi2015-01-09
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* include test-suite/coqchk in the summary logGravatar Enrico Tassi2014-12-27
* new test for coqchkGravatar Enrico Tassi2014-12-26
* Test suite: keep message in sync with actual file deletions.Gravatar Xavier Clerc2014-12-11
* typoGravatar Enrico Tassi2014-12-10
* test-suite: few tests for ".v -> .vi -> .vo" compilation chainGravatar Enrico Tassi2014-12-10
* Fix test flags for fake_ideGravatar Enrico Tassi2014-11-27
* Use return code to classify anomalies as active open bugs.Gravatar Xavier Clerc2014-11-14
* Classify segfaults as failures in opened bugs.Gravatar Xavier Clerc2014-10-03
* Classify segfaults as failures in opened bugsGravatar Xavier Clerc2014-10-03
* Added make dependency in %.out in output tests.Gravatar Hugo Herbelin2014-10-02
* Updating to the new use of 3 universes, after Hurkens is simplified.Gravatar Hugo Herbelin2014-10-01
* Reductionops: (Co)Fixpoints are always refolded during iotaGravatar Pierre Boutillier2014-09-18
* Undo prints only if coqtop || emacsGravatar Enrico Tassi2014-09-16
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* fixup fakeide test-suiteGravatar Pierre Boutillier2014-07-24
* Update test-suite Makefile to handle coq-prog-argsGravatar Jason Gross2014-05-02
* Adapt test-suite to -I is ML onlyGravatar Pierre Boutillier2014-04-09
* Remove option -g as it is non-portable yet does not have any effect on the te...Gravatar Guillaume Melquiond2014-04-04
* fake_ide: ported to spawnGravatar Enrico Tassi2014-02-10
* Testsuite: flatten the 'bugs/opened' directory.Gravatar xclerc2013-11-29
* Testsuite: remove the logic for 'bugs/opened/shouldnotsucceed' (unused)Gravatar xclerc2013-11-28
* fake_ide: ported to Document + 2 tests for editing a proof (locally)Gravatar gareuselesinge2013-10-10
* Regression test suite for STMGravatar gareuselesinge2013-10-03
* Fix name clash in "failure/inductive.v".Gravatar xclerc2013-09-20
* Execute tests from the "bugs/closed" directory.Gravatar xclerc2013-09-20
* Use "Fail" rather than rely on exit code.Gravatar xclerc2013-09-20
* Hurkens' paradox on Type (r15973 and r15977) needs two (non-Set)Gravatar herbelin2012-11-18
* Fix test-suite output/* in benchGravatar pboutill2012-10-17
* test-suite: fix grep rule for output testsGravatar pboutill2012-09-04
* test-suite uses coqtop instead of coqtop.byteGravatar pboutill2012-09-04