coq - The formal proof system

Age	Commit message (Expand)	Author
2020-07-06	Merge PR #11604: Primitive persistent arrays	Pierre-Marie Pédrot
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-07-01	Add a test for Ltac2 parsing of parameterized types.	Pierre-Marie Pédrot
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
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