coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	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