coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-08-29	A new step of restructuration of notations.	Hugo Herbelin
	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).
2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík

2017-07-25	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias
	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`
2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias

2017-06-07	Put "ssreflect" behind "API".	Matej Košík

2017-06-06	Merge the ssr plugin.	Maxime Dénès