coq - The formal proof system

Age	Commit message (Expand)	Author
2014-04-28	Fixing #3293 (eta-expansion at "match" printing time was failing	Hugo Herbelin
2014-03-01	Never suppress the typing constraint of bound variables whose name was	Pierre-Marie Pédrot
2014-02-28	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
2013-12-19	test-suite/output/Notations : evar number change	Pierre Boutillier
2013-12-02	Test suite: update output reference.	xclerc
2013-12-02	Print logical name rather than path (thus allowing reproducible tests).	xclerc
2013-11-03	test-suite fixup	pboutill
2013-10-08	Fixing 2 output test-suites.	ppedrot
2013-09-03	Fixing some tests from the test-suite.	ppedrot
2013-08-08	Fix testsuite so that it works with STM	gareuselesinge
2013-07-29	better error message for unexpected renaming (closes #2987)	gareuselesinge
2013-05-09	Updating some output tests in test-suite:	herbelin
2013-04-17	Renaming SearchAbout into Search and Search into SearchHead.	herbelin
2013-04-17	Using Parameter instead of Variable in test-suite/output	herbelin
2013-03-30	Continuation of r16346 on filtering local definitions. Refined	herbelin
2013-02-25	Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...	pboutill
2013-02-17	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-01-18	Unset Asymmetric Patterns	pboutill
2012-12-18	Fixing parsing of specific primitive tokens used as notations for patterns	herbelin
2012-12-04	Revised the strategy for automatic insertion of spaces when printing	herbelin
2012-11-17	Update output/Search.out after hint-related extra defs in Peano	letouzey
2012-07-21	Fixing bug #2835 (the rationale for printing notations was not	herbelin
2012-07-06	Minor fixes in the test-suite after my recent commits	letouzey
2012-06-14	Constrextern is allow to use partially applied notations	pboutill
2012-06-12	Fixing test-suite after last storm in Pp.	pboutill
2012-05-15	Notations are back in the "in" clause of pattern matching.	pboutill
2012-04-06	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin
2012-03-20	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin
2012-03-02	Noise for nothing	pboutill
2012-02-14	Arguments supports extra notation scopes	gareuselesinge
2012-01-31	Fix consequence of pp bugfix in testsuite	pboutill
2012-01-20	Notations with binders: Accepting using notations for functional terms	herbelin
2012-01-16	Parameters in pattern first step.	pboutill
2011-12-19	Arguments: check rename even if no implicit is specified	gareuselesinge
2011-12-17	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-07	Adapting test Existentials to new numbering strategy of evars (r14764).	herbelin
2011-12-06	Minor fixes to Arguments	gareuselesinge
2011-12-04	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-11-21	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-10-25	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey
2011-09-22	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-08-10	Fixing printing bug with last trailing non-maximally implicit	herbelin