coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
* \|	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 output test Notations2.	Hugo Herbelin	2016-04-22
*	Fixing #4677 (collision of a global variable and of a local variable	Hugo Herbelin	2016-04-19
*	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
*	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
*	Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)	letouzey	2011-03-16
*	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