coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
\|
*	Put "ssreflect" behind "API".	Matej Košík	2017-06-07
\|
*	Merge the ssr plugin.	Maxime Dénès	2017-06-06