coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Added a test for bug #3088.	ppedrot	2013-08-01
*	Tentative fix for #3054: we refresh universes in a term generated	ppedrot	2013-07-29
*	better error message for unexpected renaming (closes #2987)	gareuselesinge	2013-07-29
*	Fixing bug #3093 by adding the asked test case.	ppedrot	2013-07-25
*	More dynamic argument scopes	letouzey	2013-07-17
*	Continuing r16621 on injection intro-patterns:	herbelin	2013-07-10
*	Revising r16550 about providing intro patterns for applying injection:	herbelin	2013-07-09
*	Bugfix: Fixing #3050	ppedrot	2013-06-27
*	Fix [setoid_rewrite] forgetting some evars that are produced when typecheckin...	msozeau	2013-06-10
*	Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as an	herbelin	2013-06-02
*	Fixing a regression in unification introduced in r16205 (error raised	herbelin	2013-05-14
*	Updating some output tests in test-suite:	herbelin	2013-05-09
*	A uniformization step around understand_* and interp_* functions.	herbelin	2013-05-09
*	Protection against "Bad recursive type" in w_unify0 (bug #3036).	herbelin	2013-05-08
*	Declaration of multiple hypotheses or parameters now share typing	herbelin	2013-05-08
*	Share more information between constructors and arity of an inductive	herbelin	2013-05-08
*	Moved isolated test params_ind.v to Inductive.v.	herbelin	2013-05-08
*	Hack to solve a "Bad recursive type" anomaly.	herbelin	2013-05-05