coq - The formal proof system

Age	Commit message (Expand)	Author
2019-10-29	Document the ability to bind notation arguments in Ltac2.	Pierre-Marie Pédrot
2019-10-18	Allow to pass Ltac1 values to Ltac2 quotations.	Pierre-Marie Pédrot
2019-08-08	Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involv...	Maxime Dénès
2019-08-02	Copy edit the Ltac2 documentation	Tej Chajed
2019-07-29	Document changes by PR 10324	Vincent Laporte
2019-07-28	Update documentation on tokens, use "int" and "num"	Jim Fehrle
2019-06-25	Give a functional type to Ltac1 quotations with a context.	Pierre-Marie Pédrot
2019-06-25	Documenting the Ltac2 change.	Pierre-Marie Pédrot
2019-06-06	[Ltac2] Interpretation scopes in “constr” arguments of tactic notations	Vincent Laporte
2019-05-23	Merge PR #10195: Minor Ltac2 documentation fix: type parameters are optional.	Clément Pit-Claudel
2019-05-23	Define many undefined tokens, and other misc fixes.	Théo Zimmermann
2019-05-22	Ltac2 doc fix: syntax for extending an open variant type.	Théo Zimmermann
2019-05-20	Minor Ltac2 documentation fix: type parameters are optional.	Théo Zimmermann
2019-05-16	[refman] Introduce syntax for alternatives in notations	Clément Pit-Claudel
2019-05-12	[refman] Use 'flag' instead of 'opt' for 'Ltac2 Debug'	Clément Pit-Claudel
2019-05-07	Integrate build and documentation of Ltac2	Maxime Dénès