coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Typo in test InitSyntax.out	herbelin	2011-04-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14085 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed notation printing bug when curly brackets are involved (requests	herbelin	2011-04-28
\| \| \| \| \| \| \| \| \| \| \| \| \|	for adding spaces were not taken into account in notations containing patterns of the form "{ ident symbol", paradoxically resulting in adding extra spaces, e.g. when printing the type "{ x \| P x }" of "exist", due to interferences with the heuristic for adding breaking points in Metasyntax.make_hunk). Also adapted output of test InitSyntax.v after commit r14018 improved the printing of "ex P" and "sig P". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14073 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Factorisation des paramètres dans l'affichage des inductifs	herbelin	2007-07-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9436 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adaptation au passage de sig2 dans Type	herbelin	2006-05-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8870 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ avec les particularités de l'afficheur v7 de la V8	herbelin	2004-12-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6450 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-03-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3770 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2003-03-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3731 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	herbelin	2003-01-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3516 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction	coq	2002-08-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2976 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test syntaxe des constructions de l'état initial	herbelin	2001-10-17
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2132 85f007b7-540e-0410-9357-904b9bb8a0f7