coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
\| \| \| \| \| \| \| \| \| \| \|	The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there.
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Moving wit_unit to Stdarg.	ppedrot	2013-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16595 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Proof-of-concept: moved four easy-to-handle generic arguments to	ppedrot	2013-06-18
	their own file, Stdarg. This required a little trick to correctly handle wit_* naming. We use a dynamic table to remember exactly where those arguments come from. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16587 85f007b7-540e-0410-9357-904b9bb8a0f7