coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing #3293 (eta-expansion at "match" printing time was failing	Hugo Herbelin	2014-04-28
*	Never suppress the typing constraint of bound variables whose name was	Pierre-Marie Pédrot	2014-03-01
*	test-suite: opaque term -> opaque proof	Pierre Boutillier	2014-02-28
*	test-suite: New names for vars but the expected invariant is preserved	Pierre Boutillier	2014-02-28
*	Fix output test-suite 'simpl tactic' -> 'reduction tactics'	Pierre Boutillier	2014-02-28
*	test-suite/output/Notations : evar number change	Pierre Boutillier	2013-12-19
*	Test suite: update output reference.	xclerc	2013-12-02
*	Print logical name rather than path (thus allowing reproducible tests).	xclerc	2013-12-02
*	test-suite fixup	pboutill	2013-11-03
*	Fixing 2 output test-suites.	ppedrot	2013-10-08
*	Fixing some tests from the test-suite.	ppedrot	2013-09-03
*	Fix testsuite so that it works with STM	gareuselesinge	2013-08-08
*	better error message for unexpected renaming (closes #2987)	gareuselesinge	2013-07-29
*	Updating some output tests in test-suite:	herbelin	2013-05-09
*	Renaming SearchAbout into Search and Search into SearchHead.	herbelin	2013-04-17
*	Using Parameter instead of Variable in test-suite/output	herbelin	2013-04-17
*	Continuation of r16346 on filtering local definitions. Refined	herbelin	2013-03-30
*	Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...	pboutill	2013-02-25
*	Added propagation of evars unification failure reasons for better	herbelin	2013-02-17
*	Revised the Ltac trace mechanism so that trace breaking due to	herbelin	2013-02-17
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Fixing parsing of specific primitive tokens used as notations for patterns	herbelin	2012-12-18
*	Revised the strategy for automatic insertion of spaces when printing	herbelin	2012-12-04
*	Update output/Search.out after hint-related extra defs in Peano	letouzey	2012-11-17
*	Fixing bug #2835 (the rationale for printing notations was not	herbelin	2012-07-21
*	Minor fixes in the test-suite after my recent commits	letouzey	2012-07-06
*	Constrextern is allow to use partially applied notations	pboutill	2012-06-14
*	Fixing test-suite after last storm in Pp.	pboutill	2012-06-12
*	Notations are back in the "in" clause of pattern matching.	pboutill	2012-05-15
*	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin	2012-04-06
*	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin	2012-03-20
*	Noise for nothing	pboutill	2012-03-02
*	Arguments supports extra notation scopes	gareuselesinge	2012-02-14
*	Fix consequence of pp bugfix in testsuite	pboutill	2012-01-31
*	Notations with binders: Accepting using notations for functional terms	herbelin	2012-01-20
*	Parameters in pattern first step.	pboutill	2012-01-16
*	Arguments: check rename even if no implicit is specified	gareuselesinge	2011-12-19
*	Command Arguments: standardizing format of error messages and American spelling.	herbelin	2011-12-17
*	Bypassing the use of (currently unimplemented) "Show Script" in tests	herbelin	2011-12-17
*	Adapting test Existentials to new numbering strategy of evars (r14764).	herbelin	2011-12-07
*	Minor fixes to Arguments	gareuselesinge	2011-12-06
*	A small test for type inference (used to be a regression at some time).	herbelin	2011-12-04
*	Fixing superflous newline in output of About when no parameter is renamed.	herbelin	2011-12-04
*	Renamig support added to "Arguments"	gareuselesinge	2011-11-21
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	New Arguments vernacular	gareuselesinge	2011-11-21
*	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey	2011-10-25
*	test-suite : an additional message displayed by Notation2.v	letouzey	2011-09-22
*	Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.	letouzey	2011-09-22
*	Fixing printing bug with last trailing non-maximally implicit	herbelin	2011-08-10