coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	More toplevel value representation sharing.	Pierre-Marie Pédrot	2016-05-04
\|
*	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
\|
*	Removing dead code in Genarg.	Pierre-Marie Pédrot	2016-03-19
\|
*	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.
*	Removing the registering of default values for generic arguments.	Pierre-Marie Pédrot	2016-03-17
\|
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
\| \| \| \| \| \| \| \|	With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
*	Splitted up Genarg in four different levels:	ppedrot	2013-06-21
\| \| \| \| \| \| \| \| \| \| \| \| \|	1. Genarg itself which only defines the abstract datatypes needed. 2. Genintern, first file of interp/, defining the intern and subst functions. 3. Geninterp, first file of tactics/, defining the interp function. 4. Genprint, first file of printing/, dealing with the printers. The Genarg file has no dependency and is in lib/, so that we can put generic arguments everywhere, and in particular in ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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