coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5' into trunk	Maxime Dénès	2016-07-04
\|\
\| *	test-suite: test checking of libraries checksum.	Maxime Dénès	2016-07-04
* \|	fix test-suite/ide Makefile (stupid typo)	Enrico Tassi	2016-06-15
* \|	test-suiet: run fake_id as before pr/173 was merged	Enrico Tassi	2016-06-14
* \|	STM: code cleanup	Enrico Tassi	2016-05-10
* \|	Do that "make" in test-suite writes failures as a default together	Hugo Herbelin	2016-04-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-12-07
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\|
\| *	Adding a target report to test-suite's Makefile to get a short summary.	Hugo Herbelin	2015-12-02
* \|	New algorithm for universe cycle detections.	Jacques-Henri Jourdan	2015-12-01
\|/
*	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