coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-13	Allow scope delimiters in Ltac2 open_constr:(...) quotation.	Pierre-Marie Pédrot
2021-01-22	Add a type of format strings to Ltac2.	Pierre-Marie Pédrot
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
2020-02-14	Annotate Ltac2 match macro variables with their type.	Pierre-Marie Pédrot
2019-10-29	Fix #10615: Notation substitution for Ltac2 terms.	Pierre-Marie Pédrot
2019-06-17	Update headers of files that were stuck on older headers.	Théo Zimmermann
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