coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Introduce a Pcoq.Entry module for functions that ought to be exported.	Pierre-Marie Pédrot	2018-07-07
\| \| \| \| \| \| \| \| \| \|	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.
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias	2017-07-25
\| \| \| \| \| \| \| \| \| \| \| \|	This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
\|
*	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
\|
*	Ltac as a plugin.	Pierre-Marie Pédrot	2017-02-17
	This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.