coq - The formal proof system

Age	Commit message (Collapse)	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
	Ack-by: SkySkimmer Ack-by: Zimmi48
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
	Fixes #10909: Set Default Proof Mode is not documented.
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
	This is the dual of #10344.
2019-08-08	Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations ↵	Maxime Dénès
	involving & Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: gares Ack-by: ggonthier Ack-by: herbelin Reviewed-by: maximedenes Ack-by: vbgl
2019-08-02	Copy edit the Ltac2 documentation	Tej Chajed

2019-07-29	Document changes by PR 10324	Vincent Laporte
	White spaces are forbidden in the “&ident” syntax for ltac2 references.
2019-07-28	Update documentation on tokens, use "int" and "num"	Jim Fehrle
	for integers and natural nums
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	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
	Reviewed-by: cpitclaudel Reviewed-by: ppedrot
2019-05-23	Define many undefined tokens, and other misc fixes.	Théo Zimmermann
	Progress towards #9411, extracted from #10118, rebased ontop of #10192.
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
	Closes GH-8482.
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
	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.