coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin	2012-04-06
*	Notations with binders: Accepting using notations for functional terms	herbelin	2012-01-20
*	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
*	Partly revert commit r14389 about relaxing the condition for being a keyword	herbelin	2011-08-10
*	Be a bit less aggressive in declaring idents as keywords in notations	herbelin	2011-08-08
*	Fixing output of Notations2.v test messed up in r14060	herbelin	2011-04-27
*	Fixing and completing interpretation of let's in notations for iterated binders.	herbelin	2011-04-25
*	Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".	herbelin	2011-04-15
*	Fixing multiple printing bugs with "Notation f x := ..."	herbelin	2011-04-08
*	Did that adding a rule for printing applications as "f(x)" works.	herbelin	2011-03-31
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Added printing of recursive notations in cases pattern (supported by wish 2248).	herbelin	2010-06-14
*	Fixed some printing bugs.	herbelin	2010-04-18
*	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin	2009-04-25
*	Fixing #2044 (bad printing of primitive notation at the head of	herbelin	2009-02-06