coq - The formal proof system

Age	Commit message (Expand)	Author
2020-05-12	documenting with examples the dynamic behaviour of Ltac2 Set	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-04-26	Convert syntax extensions chapter to prodn	Jim Fehrle
2020-02-28	Merge PR #11423: Convert Vernacular section of gallina chapter to use prodn	Théo Zimmermann
2020-02-28	Convert Gallina Vernac to use prodn	Jim Fehrle
2020-02-24	Make it clear how to import Ltac2	Clément Pit-Claudel
2020-01-14	Document the Set Default Proof Mode command.	Pierre-Marie Pédrot
2019-12-22	[refman] Mention Ltac2 in intro.	Théo Zimmermann
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