coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-05-17	Ltac2: add notations for eval cbv in ... and other in place reductions	Michael Soegtrop

2020-05-11	More tests of rebinding Ltac2 definitions	Kenji Maillard

2020-05-11	Correcting ltac2's documentation on values turning test into proper check.	Kenji Maillard

2020-05-11	Allow to rebind the old value of a mutable Ltac2 entry.	Pierre-Marie Pédrot

2020-03-18	Adding a round-trip test for binders.	Pierre-Marie Pédrot

2020-03-18	Actually use the binder type for Ltac2 that should be used in the kernel.	Pierre-Marie Pédrot
	That is, it contains the type of the binder so as not to rely on the relevance explicitly.
2020-03-03	Ltac2: Add notation for enough and eenough	Michael Soegtrop

2020-02-08	Resolve #10342 : [Ltac2] Add array library	Michael Soegtrop

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-10-18	Allow to pass Ltac1 values to Ltac2 quotations.	Pierre-Marie Pédrot
	This is the dual of #10344.
2019-09-24	Fix #10783: use binder_annot in Ltac2.Constr.Unsafe.kind	Gaëtan Gilbert

2019-06-25	Give a functional type to Ltac1 quotations with a context.	Pierre-Marie Pédrot
	This looks more principled, and doesn't require as much tinkering with the typing implementation.
2019-06-25	Adding the ability to transfer Ltac2 variables to Ltac1 quotations.	Pierre-Marie Pédrot

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.