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.
*	[api] Remove Misctypes.	Emilio Jesus Gallego Arias	2018-06-12
\| \| \| \|	We move the last 3 types to more adequate places.
*	[notations] Split interpretation and parsing of notations	Emilio Jesus Gallego Arias	2018-05-31
\| \| \| \| \| \| \| \|	Previously to this patch, `Notation_term` contained information about both parsing and notation interpretation. We split notation grammar to a file `parsing/notation_gram` as to make `interp/` not to depend on some parsing structures such as entries.
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
\| \| \| \| \| \| \| \| \|	We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
*	A new step of restructuration of notations.	Hugo Herbelin	2017-08-29
\| \| \| \| \| \| \|	This allows to issue a more appropriate message when a notation with a { } cannot be defined because of an incompatible level. E.g.: Notation "{ A } + B" := (sumbool A B) (at level 20).
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-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
\|
*	Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.	Hugo Herbelin	2017-05-16
\|
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|
*	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.