coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Do not display the status of monomorphic constants unless in ↵	Guillaume Melquiond	2015-03-09
\| \| \| \|	universe-polymorphism mode.
*	Upgrading output tests.	Hugo Herbelin	2014-08-12
\| \| \| \| \| \| \| \| \| \| \| \|	output/Arguments.v output/ArgumentsScope.v output/Arguments_renaming.v output/Cases.v output/Implicit.v output/PrintInfos.v output/TranspModType.v Main changes: monomorphic -> not universe polymorphic, Peano vs Nat
*	Fixing output test-suite: since universe polymorphism, the Print command	Pierre-Marie Pédrot	2014-05-08
\| \| \| \|	shows the polymorphism status of the term.
*	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
*	Correction de quelques défauts d'affichage (notations sous "as" pour	herbelin	2007-10-05
\| \| \| \| \| \| \| \|	filtrage; sauts de line intempestifs dans pretty.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10179 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
*	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 *	herbelin	2003-10-10
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4585 85f007b7-540e-0410-9357-904b9bb8a0f7