coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adding a test for bug #3023.	Pierre-Marie Pédrot	2014-01-25
*	Test case containing a proof of false due to a DeBruijn off-by-one error in the	Maxime Dénès	2014-01-15
*	rename Paral-ITP demo file	Enrico Tassi	2014-01-13
*	Paral-ITP demo: better comments	Enrico Tassi	2014-01-13
*	STM: fix very simple demo	Enrico Tassi	2014-01-13
*	Fix bug#2080: error message on Ltac name clash with primitive tactics	xclerc	2014-01-10
*	fix simple test for paral-itp	Enrico Tassi	2014-01-06
*	Add a test suite file for Ltac's "+" tactical.	Arnaud Spiwack	2014-01-06
*	Test case for the buggy commutative cut subterm rule.	Maxime Dénès	2013-12-21
*	micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...	Frédéric Besson	2013-12-20
*	test-suite/output/Notations : evar number change	Pierre Boutillier	2013-12-19
*	Missing Fail in r16792	Pierre Boutillier	2013-12-19
*	test guard condition against feature incompatible with prop-ext	Bruno Barras	2013-12-17
*	Tentative fix of the guardedness checker by Christine and me. All stdlib and ...	Matthieu Sozeau	2013-12-17
*	Added test-suite for bug #2990.	Pierre-Marie Pédrot	2013-12-16
*	Better unification for [projT1] and [proj1_sig].	Jason Gross	2013-12-12
*	Remove duplicate test-suite file.	Arnaud Spiwack	2013-12-06
*	Fix the refine related test-suite files to account for the new refine.	Arnaud Spiwack	2013-12-06
*	Test case for bug#2848.	xclerc	2013-12-02
*	Test suite: update output reference.	xclerc	2013-12-02
*	Print logical name rather than path (thus allowing reproducible tests).	xclerc	2013-12-02
*	Testsuite: flatten the 'bugs/opened' directory.	xclerc	2013-11-29
*	Testsuite: remove the logic for 'bugs/opened/shouldnotsucceed' (unused)	xclerc	2013-11-28
*	test-suite fixup	pboutill	2013-11-03
*	Document: undoing inside a focused zone does not require unfocusing	gareuselesinge	2013-10-10
*	fake_ide: ported to Document + 2 tests for editing a proof (locally)	gareuselesinge	2013-10-10
*	Fixing 2 output test-suites.	ppedrot	2013-10-08
*	fake_ide: speak the new protocol	gareuselesinge	2013-10-07
*	Regression test suite for STM	gareuselesinge	2013-10-03
*	demo file for paral-itp	gareuselesinge	2013-10-01
*	Fix name clash in "failure/inductive.v".	xclerc	2013-09-20
*	Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.	xclerc	2013-09-20
*	Merge "inductive?.v" tests into a single "inductive.v" test.	xclerc	2013-09-20
*	Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.	xclerc	2013-09-20
*	Get rid of "shouldfail" subdirectory by moving tests to parent directory.	xclerc	2013-09-20
*	Wrong bug identifier.	xclerc	2013-09-20
*	Execute tests from the "bugs/closed" directory.	xclerc	2013-09-20
*	Update test for bug 2846 in order to use "Fail".	xclerc	2013-09-20
*	Use "Fail" rather than rely on exit code.	xclerc	2013-09-20
*	Uminus.v : prepare this test file for the use of Fail	letouzey	2013-09-19
*	universes-buraliforti-redef.v : repair a match after Pierre B. syntax changes	letouzey	2013-09-19
*	Fixing some tests from the test-suite.	ppedrot	2013-09-03
*	* test-suite/success/Unicode_utf8:	regisgia	2013-09-02
*	Trickyer test for Paral-ITP	gareuselesinge	2013-08-30
*	Universe counters on slaves are in sync with master	gareuselesinge	2013-08-20
*	Test for Paral-ITP	gareuselesinge	2013-08-08
*	Coqide ported to STM	gareuselesinge	2013-08-08
*	Fix testsuite so that it works with STM	gareuselesinge	2013-08-08
*	Added test for bug #2846.	ppedrot	2013-08-04
*	Added a test for bug #3062.	ppedrot	2013-08-04