coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-03-13	Allow scope delimiters in Ltac2 open_constr:(...) quotation.	Pierre-Marie Pédrot
	Fixes #12806: Ltac2 Notation's open_constr should accept scope stacks.
2021-01-22	Add a type of format strings to Ltac2.	Pierre-Marie Pédrot
	It provides an abstract type of well-typed format strings, a scope to parse them and a minimal printf-like API.
2020-10-10	Add location in existential variable names (CEvar/GEvar).	Hugo Herbelin

2020-07-18	Clarify the Ltac2 invalid identifier message.	Pierre-Marie Pédrot

2020-07-18	Better location for match! pattern variables in Ltac2.	Pierre-Marie Pédrot

2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-02-14	Annotate Ltac2 match macro variables with their type.	Pierre-Marie Pédrot
	This prevents some warnings to be dropped when the variables are not used at the right type. See #11603 for a motivation.
2019-10-29	Fix #10615: Notation substitution for Ltac2 terms.	Pierre-Marie Pédrot
	We implement a new type of "preterms" that represent untyped ASTs, corresponding to glob_expr in the ML implementations. Ltac2 quotations inside notations are provided with such preterms, and have to pretype them in order to do anything of relevance with them.
2019-06-17	Update headers of files that were stuck on older headers.	Théo Zimmermann
	Most of these files were introduced after #6543 but used older headers copied from somewhere else.
2019-06-06	[Ltac2] Interpretation scopes in “constr” arguments of tactic notations	Vincent Laporte

2019-05-07	Integrate build and documentation of Ltac2	Maxime Dénès
	Since Ltac2 cannot be put under the stdlib logical root (some file names would clash), we move it to the `user-contrib` directory, to avoid adding another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego. Thanks to @Zimmi48 for the thorough documentation review and the numerous suggestions.