coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-05-04	More toplevel value representation sharing.	Pierre-Marie Pédrot

2016-05-04	Moving the Val module to Geninterp.	Pierre-Marie Pédrot

2016-03-19	Removing dead code in Genarg.	Pierre-Marie Pédrot

2016-03-17	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot
	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.
2016-03-17	Removing the registering of default values for generic arguments.	Pierre-Marie Pédrot

2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
	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.
2013-06-21	Splitted up Genarg in four different levels:	ppedrot
	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
2013-06-19	Moving wit_unit to Stdarg.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16595 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-18	Proof-of-concept: moved four easy-to-handle generic arguments to	ppedrot
	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