coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-03-25	[pcoq] Inline the exported Gramlib interface instead of exposing it as G	Emilio Jesus Gallego Arias

2020-03-25	[parsing] Remove extend AST in favor of gramlib constructors	Emilio Jesus Gallego Arias
	We remove Coq's wrapper over gramlib's grammar constructors.
2020-03-25	[parsing] Make grammar extension type private.	Emilio Jesus Gallego Arias
	After the gramlib merge and the type-safe interface added to it, the grammar extension type is redundant; we thus make it private as a first step on consolidating it with the one in gramlib's.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-03-31	Multiple payload types in tokens	Pierre Roux
	Instead of just string (and empty strings for tokens without payload)
2018-11-17	[vernacextend] Consolidate extension points API	Emilio Jesus Gallego Arias
	We group the extension API and datatypes under `Vernacextend`. This means that the base plugin dependency is now `coq.vernac` from `coq.stm`. This is quite important as for example the LSP server won't like to link the STM in. LTAC still depends on the STM by means of the ltac_profile part tho. The next step could be to move the extension point below `Vernacexpr`.
2018-10-02	Pass unnamed arguments to ML macros.	Pierre-Marie Pédrot
	This was imposing a bit of useless burden on the API for no good reason.
2018-07-12	Statically typecheck the VERNAC EXTEND wrapper.	Pierre-Marie Pédrot
	This moves the typing code from the macro expansion to the extension registering mechanism, bringing in more static safety. We also seize the opportunity to remove dead code in the macro.
2018-07-07	Introduce a Pcoq.Entry module for functions that ought to be exported.	Pierre-Marie Pédrot
	We deprecate the corresponding functions in Pcoq.Gram. The motivation is that the Gram module is used as an argument to Camlp5 functors, so that it is not stable by extension. Enforcing that its type is literally the one Camlp5 expects ensures robustness to extension statically. Some really internal functions have been bluntly removed. It is unlikely that they are used by external plugins.
2018-05-27	[api] [parsing] Move Egram* to `vernac/`	Emilio Jesus Gallego Arias
	The extension mechanism is specific to metasyntax and vernacinterp, thus it makes sense to place them next to each other. We also fix the META entry for the `grammar` camlp5 plugin.