coq - The formal proof system

Age	Commit message (Expand)	Author
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
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
2019-10-18	Allow to pass Ltac1 values to Ltac2 quotations.	Pierre-Marie Pédrot
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
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