coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-04-17	Properly pass the Ltac2 notation level to the gramlib API.	Pierre-Marie Pédrot
	For some reason I was confusing the position and the level in the previous version of the code. Fixes #11866: Ltac2 Notations do not respect precedence.
2021-04-16	Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.	coqbot-app[bot]
	Reviewed-by: JasonGross
2021-03-23	Merge PR #13774: Allow to register deprecation status in Ltac2 term and ↵	Michael Soegtrop
	notation declarations Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-03-13	Documenting the changes.	Pierre-Marie Pédrot

2021-03-10	Add documentation.	Pierre-Marie Pédrot

2021-03-10	Regenerate the Ltac2 syntax for documentation.	Pierre-Marie Pédrot

2021-03-08	Convert 2nd part of rewriting chapter to prodn	Jim Fehrle

2021-01-18	Merge PR #13574: Simplistic patch to fix #10113: turn Ltac2's `pattern:` ↵	Pierre-Marie Pédrot
	into `pat:` Ack-by: Zimmi48 Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-12-30	Convert rewriting and proof-mode chapters to prodn	Jim Fehrle

2020-12-04	turn Ltac2's `pattern:` into `pat:`	Kenji Maillard

2020-11-24	Convert auto chapter to prodn	Jim Fehrle

2020-11-10	Convert logic.rst to prodn	Jim Fehrle

2020-11-09	Add global version of OPTINREF	Jim Fehrle

2020-11-09	[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.	Théo Zimmermann
	The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version.
2020-11-04	Regenerate the grammar description file.	Pierre-Marie Pédrot

2020-11-04	Document the syntax addition.	Pierre-Marie Pédrot

2020-10-20	Add some missing smallcaps.	Théo Zimmermann

2020-09-11	Turn integer into natural in several mlgs	Pierre Roux
	Negative values had no meaning there. Those were spotted by Hugo Herbelin while reviewing #12979 .
2020-09-11	[refman] Rename int to integer	Pierre Roux

2020-09-11	[refman] Rename num to natural	Pierre Roux

2020-08-25	Convert ltac2 chapter to use prodn, update syntax	Jim Fehrle

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.