coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Added printing of recursive notations in cases pattern (supported by wish 2248).	herbelin	2010-06-14
\| \| \| \| \| \| \|	Note that the code is no longer in constrextern.ml but in topconstr.ml where the code for reversing notations of term already was. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13132 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed some printing bugs.	herbelin	2010-04-18
\| \| \| \| \| \| \| \| \| \|	- Notations with coercions to funclass inserted were not working any longer since r11886. Made a fix but maybe should we eventually type the notations so that they have a canonical form (and in particular with coercions pre-inserted?). - Improved spacing management in printing extra tactic arguments "by" and "in". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12951 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin	2009-04-25
\| \| \| \| \| \| \| \| \| \|	- Adding test file related to commit 12080 (bug #2091). - Cleaning old parsing stuff from 8.0. - Support for camlp5 in base_include. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12106 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing #2044 (bad printing of primitive notation at the head of	herbelin	2009-02-06
	coercion to funclass) [added a new notation output test as the initial one is quite saturated in miscellaneous notations]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11886 85f007b7-540e-0410-9357-904b9bb8a0f7