aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/user-extensions/syntax-extensions.rst
AgeCommit message (Expand)Author
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-05-15Merge PR #12239: Split Gallina, Gallina ext and most of CIC chapters into mul...Clément Pit-Claudel
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
2020-05-14Fix conflicts with latest master.Théo Zimmermann
2020-05-14Add some markers of origin.Théo Zimmermann
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-05-13Documenting notations with both terms and binders.Hugo Herbelin
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-09[doc] Add hexadecimal numeralsPierre Roux
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-03-09Remove some productionlistsJim Fehrle
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
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-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
2020-02-24added sphinx docAbhishek Anand (optiplex7010@home)
2020-02-23Documenting inheritance of implicit arguments and scopes in notations.Hugo Herbelin
2020-02-19Short allusion in refman on the existence of a generic and specific format.Hugo Herbelin
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
2020-02-16Custom entries: accept that no level is mentioned for a subentry.Hugo Herbelin
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
2019-10-28Add support for Sorts in numeral notationsJason Gross
2019-10-23Better wording for "Show Proof" and fix typosJim Fehrle
2019-10-22documentation fixesAntonio Nikishaev
2019-06-16Deprecate "intro_pattern" in tactic notations in favor of "simple_intropattern".Hugo Herbelin
2019-05-24Merge PR #10167: do not parse `|` as infix in patterns; parse `|}` as `|` `}`Emilio Jesus Gallego Arias
2019-05-23Merge PR #10217: Less undefined tokensClément Pit-Claudel
2019-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
2019-05-23Update doc/sphinx/user-extensions/syntax-extensions.rstMaxime Dénès
2019-05-23Update doc/sphinx/user-extensions/syntax-extensions.rstMaxime Dénès
2019-05-23Update doc/sphinx/user-extensions/syntax-extensions.rstMaxime Dénès
2019-05-23Define many undefined tokens, and other misc fixes.Théo Zimmermann
2019-05-23Update `Bind Scope` documentation to reflect 3d09e39dd423d81c6af3e991d5b282ea...Maxime Dénès
2019-05-22[refman] Misc fixes (mostly missing '@' signs)Clément Pit-Claudel
2019-05-22[refman] Give explicit names to the various 'Arguments' commandsClément Pit-Claudel
2019-05-21Fixing typos - Part 1JPR
2019-05-19[refman] Add a .. cmd:: header for Reserved Notation and Reserved InfixClément Pit-Claudel
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
2019-04-30Split changes between main changes and other changes (no repetition).Théo Zimmermann
2019-04-29Revert #8187Vincent Laporte
2019-04-05Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)Emilio Jesus Gallego Arias
2019-04-03Minor correction to numeral notations docJason Gross
2019-04-02Update documentationPierre Roux
2019-04-01Update numeral notation printing docJason Gross
2019-02-28[sphinx] Add warn option to coqtop directive.Théo Zimmermann
2019-02-12Fix failing coqtops in syntax-extensions.rstGaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2019-01-25[Numeral notations] Lazy resolution of decimal typesVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:30:10 +0000