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-07-13	Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.	Pierre-Marie Pédrot

2017-06-16	Removing Proof_type from the API.	Pierre-Marie Pédrot
	Unluckily, this forces replacing a lot of code in plugins, because the API defined the type of goals and tactics in Proof_type, and by the no-alias rule, this was the only one. But Proof_type was already implicitly deprecated, so that the API should have relied on Tacmach instead.
2017-06-16	Remove the last use of the low-level Proof_type API in ssr.	Pierre-Marie Pédrot

2017-06-15	Merge PR#719: Constrexpr.Numeral without bigint	Maxime Dénès

2017-06-14	Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").	Maxime Dénès

2017-06-14	Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)	Pierre Letouzey
	This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml
2017-06-13	Dualize the unsafe flag of refine into typecheck and make it mandatory.	Pierre-Marie Pédrot

2017-06-12	Merge PR#718: API cleanup: aliases	Maxime Dénès

2017-06-10	Remove remaining vo.itarget files (obsolete since PR #499)	Pierre Letouzey

2017-06-10	Remove (useless) aliases from the API.	Matej Košík

2017-06-09	A fix to #5414 (ident bound by ltac names now known for "match").	Hugo Herbelin
	Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let".
2017-06-07	Put "ssreflect" behind "API".	Matej Košík

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