aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine/ltac2.rst
AgeCommit message (Expand)Author
2021-04-17Properly pass the Ltac2 notation level to the gramlib API.Pierre-Marie Pédrot
2021-04-16Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.coqbot-app[bot]
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and notat...Michael Soegtrop
2021-03-13Documenting the changes.Pierre-Marie Pédrot
2021-03-10Add documentation.Pierre-Marie Pédrot
2021-03-10Regenerate the Ltac2 syntax for documentation.Pierre-Marie Pédrot
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-01-18Merge PR #13574: Simplistic patch to fix #10113: turn Ltac2's `pattern:` into...Pierre-Marie Pédrot
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-12-04turn Ltac2's `pattern:` into `pat:`Kenji Maillard
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-09Add global version of OPTINREFJim Fehrle
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
2020-11-04Regenerate the grammar description file.Pierre-Marie Pédrot
2020-11-04Document the syntax addition.Pierre-Marie Pédrot
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-09-11Turn integer into natural in several mlgsPierre Roux
2020-09-11[refman] Rename int to integerPierre Roux
2020-09-11[refman] Rename num to naturalPierre Roux
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-05-12documenting with examples the dynamic behaviour of Ltac2 SetKenji Maillard
2020-05-11Correcting ltac2's documentation on values turning test into proper check.Kenji Maillard
2020-05-11Allow to rebind the old value of a mutable Ltac2 entry.Pierre-Marie Pédrot
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-02-28Merge PR #11423: Convert Vernacular section of gallina chapter to use prodnThéo Zimmermann
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
2020-02-24Make it clear how to import Ltac2Clément Pit-Claudel
2020-01-14Document the Set Default Proof Mode command.Pierre-Marie Pédrot
2019-12-22[refman] Mention Ltac2 in intro.Théo Zimmermann
2019-10-29Document the ability to bind notation arguments in Ltac2.Pierre-Marie Pédrot
2019-10-18Allow to pass Ltac1 values to Ltac2 quotations.Pierre-Marie Pédrot
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involv...Maxime Dénès
2019-08-02Copy edit the Ltac2 documentationTej Chajed
2019-07-29Document changes by PR 10324Vincent Laporte
2019-07-28Update documentation on tokens, use "int" and "num"Jim Fehrle
2019-06-25Give a functional type to Ltac1 quotations with a context.Pierre-Marie Pédrot
2019-06-25Documenting the Ltac2 change.Pierre-Marie Pédrot
2019-06-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
2019-05-23Merge PR #10195: Minor Ltac2 documentation fix: type parameters are optional.Clément Pit-Claudel
2019-05-23Define many undefined tokens, and other misc fixes.Théo Zimmermann
2019-05-22Ltac2 doc fix: syntax for extending an open variant type.Théo Zimmermann
2019-05-20Minor Ltac2 documentation fix: type parameters are optional.Théo Zimmermann
2019-05-16[refman] Introduce syntax for alternatives in notationsClément Pit-Claudel
2019-05-12[refman] Use 'flag' instead of 'opt' for 'Ltac2 Debug'Clément Pit-Claudel
2019-05-07Integrate build and documentation of Ltac2Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:38:01 +0000