aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/Makefile
Commit message (Expand)AuthorAge
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Adding a target report to test-suite's Makefile to get a short summary.Gravatar Hugo Herbelin2015-12-02
* 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
* In the output tests, ignore dynlink messagesGravatar letouzey2012-08-24
* No more coqtop.opt, produce directly a coqtop binaryGravatar letouzey2012-08-23
* Add distclean back to test-suite/MakefileGravatar glondu2012-01-14
* Fix test-suite/ide for repository compiled without -local (fix #2600)Gravatar letouzey2011-09-19
* Various fixes in the MakefilesGravatar letouzey2011-09-17
* test-suite/ide: misc improvementGravatar letouzey2011-09-06
* fake_ide: a short program to mimic an ide talking to coqtop -ideslaveGravatar letouzey2011-09-05
* fix bug 2510: xml test is in the summary if it failsGravatar pboutill2011-06-22
* MacOS compatibilityGravatar pboutill2011-02-10