coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Applying same convention as in Definition for printing type in a let in.	Hugo Herbelin	2017-03-24
*	Fixing a few other inconsistencies with notations.	Hugo Herbelin	2016-10-17
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-14
\|\
\| *	Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.	Hugo Herbelin	2016-09-12
* \|	Removing a source of clash with multiple recursive patterns in notations.	Hugo Herbelin	2016-07-19
* \|	Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).	Hugo Herbelin	2016-06-24
* \|	Revert "A heuristic to add parentheses in the presence of rules such as"	Hugo Herbelin	2016-04-27
* \|	A heuristic to add parentheses in the presence of rules such as	Hugo Herbelin	2016-04-27
\|/
*	Fixing #4677 (collision of a global variable and of a local variable	Hugo Herbelin	2016-04-19
*	Adapting output tests to the removal of the new token warning and to	Hugo Herbelin	2014-10-21
*	Never suppress the typing constraint of bound variables whose name was	Pierre-Marie Pédrot	2014-03-01
*	Updating some output tests in test-suite:	herbelin	2013-05-09
*	Revised the strategy for automatic insertion of spaces when printing	herbelin	2012-12-04
*	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