coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Univs: the stdlib now needs 5 universes	Matthieu Sozeau	2015-10-02
*	Updating the documentation and the toolchain w.r.t. the change in -compile.	Pierre-Marie Pédrot	2015-09-25
*	test-suite: Fix test-suite Makefile	Matthieu Sozeau	2015-07-07
*	Flag -test-mode intended to be used for ad-hoc prints in test-suite	Enrico Tassi	2015-05-29
*	camlp4: grep away warnings in output/* tests	Enrico Tassi	2015-03-30
*	There was one more universe needed due to the use of now non-universe-polymor...	Matthieu Sozeau	2015-01-18
*	Back to 4 expected universes.	Matthieu Sozeau	2015-01-17
*	STM: fix handling of side effects in vio2vo	Enrico Tassi	2015-01-09
*	rename: vi -> vio	Enrico Tassi	2015-01-06
*	include test-suite/coqchk in the summary log	Enrico Tassi	2014-12-27
*	new test for coqchk	Enrico Tassi	2014-12-26
*	Test suite: keep message in sync with actual file deletions.	Xavier Clerc	2014-12-11
*	typo	Enrico Tassi	2014-12-10
*	test-suite: few tests for ".v -> .vi -> .vo" compilation chain	Enrico Tassi	2014-12-10
*	Fix test flags for fake_ide	Enrico Tassi	2014-11-27
*	Use return code to classify anomalies as active open bugs.	Xavier Clerc	2014-11-14
*	Classify segfaults as failures in opened bugs.	Xavier Clerc	2014-10-03
*	Classify segfaults as failures in opened bugs	Xavier Clerc	2014-10-03
*	Added make dependency in %.out in output tests.	Hugo Herbelin	2014-10-02
*	Updating to the new use of 3 universes, after Hurkens is simplified.	Hugo Herbelin	2014-10-01
*	Reductionops: (Co)Fixpoints are always refolded during iota	Pierre Boutillier	2014-09-18
*	Undo prints only if coqtop \|\| emacs	Enrico Tassi	2014-09-16
*	Removing dead code relative to the XML plugin.	Pierre-Marie Pédrot	2014-09-08
*	fixup fakeide test-suite	Pierre Boutillier	2014-07-24
*	Update test-suite Makefile to handle coq-prog-args	Jason Gross	2014-05-02
*	Adapt test-suite to -I is ML only	Pierre Boutillier	2014-04-09
*	Remove option -g as it is non-portable yet does not have any effect on the te...	Guillaume Melquiond	2014-04-04
*	fake_ide: ported to spawn	Enrico Tassi	2014-02-10
*	Testsuite: flatten the 'bugs/opened' directory.	xclerc	2013-11-29
*	Testsuite: remove the logic for 'bugs/opened/shouldnotsucceed' (unused)	xclerc	2013-11-28
*	fake_ide: ported to Document + 2 tests for editing a proof (locally)	gareuselesinge	2013-10-10
*	Regression test suite for STM	gareuselesinge	2013-10-03
*	Fix name clash in "failure/inductive.v".	xclerc	2013-09-20
*	Execute tests from the "bugs/closed" directory.	xclerc	2013-09-20
*	Use "Fail" rather than rely on exit code.	xclerc	2013-09-20
*	Hurkens' paradox on Type (r15973 and r15977) needs two (non-Set)	herbelin	2012-11-18
*	Fix test-suite output/* in bench	pboutill	2012-10-17
*	test-suite: fix grep rule for output tests	pboutill	2012-09-04
*	test-suite uses coqtop instead of coqtop.byte	pboutill	2012-09-04
*	In the output tests, ignore dynlink messages	letouzey	2012-08-24
*	No more coqtop.opt, produce directly a coqtop binary	letouzey	2012-08-23
*	Add distclean back to test-suite/Makefile	glondu	2012-01-14
*	Fix test-suite/ide for repository compiled without -local (fix #2600)	letouzey	2011-09-19
*	Various fixes in the Makefiles	letouzey	2011-09-17
*	test-suite/ide: misc improvement	letouzey	2011-09-06
*	fake_ide: a short program to mimic an ide talking to coqtop -ideslave	letouzey	2011-09-05
*	fix bug 2510: xml test is in the summary if it fails	pboutill	2011-06-22
*	MacOS compatibility	pboutill	2011-02-10
*	test-suite/Makefile: add a rule to build all_stdlib.v (for the bench)	glondu	2011-01-27
*	Add a test for sorting all universes of stdlib	glondu	2011-01-25