coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix consequence of pp bugfix in testsuite	pboutill	2012-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14954 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
*	or_introl is now too complicated for basic tests of ↵	pboutill	2011-07-26
\| \| \| \| \| \| \| \| \|	test-suite/output/PrintInfos.v This is due to r14296. existT should do the job. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14302 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Some fixes of the test-suite scripts	letouzey	2011-02-21
\| \| \| \| \| \| \| \|	In particular, the Fail meta-command cannot for the moment catch a Syntax Error, which is raised by Vernac.parse_sentence, before we even now that the line starts by a Fail... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13847 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
\| \| \| \| \| \| \| \| \|	Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]". This should a priori be used with care (it might be a bit disturbing seeing the same constant used with apparently incompatible signatures). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Making display of various informations about constants more modular:	herbelin	2010-10-03
	- use list of non-newline-ended phrases instead of newline-separated texts because newline-separated texts does not support well being put in boxes (e.g. ''v 2 (str"a" ++ fnl()) ++ str"b" ++ fnl()'' prints "b" at indentation 2 while to get the expected output, one would have needed to have the fnl outside the box as in ''v 2 (str"a") ++ fnl() ++ str"b" ++ fnl()'' - also reason over lists of explicitly non-empty lines instead of checking for "mt" lines to skip The reason of this is to permit nesting of printing infos. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13482 85f007b7-540e-0410-9357-904b9bb8a0f7