coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix issues in test-suite revealed by warnings.	Maxime Dénès	2016-06-29
\|
*	Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080	Jason Gross	2015-08-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change in the semantics of arguments scopes: scopes can no longer be bound to Funclass or Sortclass (this does not seem to be useful)). It is useful to have function_scope for, e.g., function composition. This allows users to, e.g., automatically interpret ∘ as morphism composition when expecting a morphism of categories, as functor composition when expecting a functor, and as function composition when expecting a function. Additionally, it is nicer to have fewer special cases in the OCaml code, and give more things a uniform syntax. (The scope type_scope should not be special-cased; this change is coming up next.) Also explicitly define [function_scope] in theories/Init/Notations.v. This closes bug #3080, Build a [function_scope] like [type_scope], or allow [Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass] We now mention Funclass and Sortclass in the documentation of [Bind Scope] again.
*	Do not display the status of monomorphic constants unless in ↵	Guillaume Melquiond	2015-03-09
\| \| \| \|	universe-polymorphism mode.
*	Adapted test file for About.	Pierre Courtieu	2014-12-15
\|
*	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 some tests from the test-suite.	ppedrot	2013-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16760 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating some output tests in test-suite:	herbelin	2013-05-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	InitSyntax, PrintInfos: consequence of r16467 which improved printing of sigT Notations2: consequence of r16470 on using notations while asked to print the body of an abbreviation Notations: fix from r16417 was incomplete (and by the way associated to a wrong commit message) names: related to commit r16205 which aligned "In environment" with the variables of the environment (maybe should it be better to still have "In environment" printed after "Error: " but I don't know how to do it with a forced newline). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16503 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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