coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Moving bug numbers to BZ# format in the test-suite.	Théo Zimmermann	2017-10-19
\| \| \| \| \|	Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
*	Fixing superflous newline in output of About when no parameter is renamed.	herbelin	2011-12-04
\| \| \| \| \| \| \| \| \|	Fixing output tests after having added flushing of warning in revisions 14747 and 14750. Moving Implicit output test to new command Arguments. Adding test of new Arguments syntax in PrintInfos.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14758 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing printing bug with last trailing non-maximally implicit	herbelin	2011-08-10
\| \| \| \| \| \| \| \|	arguments needed for correct typing of partial applications (knowing that in practice, users should anyway better declare such arguments as maximally inserted). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14404 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveaux changements autour des implicites (notamment suite à	herbelin	2007-05-06
\| \| \| \| \| \| \| \| \| \| \| \| \|	discussion avec Georges) - La notion d'insertion maximale n'est plus globale mais attachée à chaque implicite - Correction de petits bugs dans le calcul des implicites - Raffinement de la notion "sous contexte" pour l'affichage des coercions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9817 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
*	* empty log message *	herbelin	2003-10-10
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4585 85f007b7-540e-0410-9357-904b9bb8a0f7