aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/user-extensions
AgeCommit message (Expand)Author
2020-09-14Merge PR #13022: Fixing documentation relatively to example of use of extra s...coqbot-app[bot]
2020-09-13Fixing documentation relatively to example of use of extra spaces in notations.Hugo Herbelin
2020-09-11[numeral notation] Improve documentationPierre Roux
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-09-11[refman] Explicit integer and naturalPierre Roux
2020-09-11[refman] Rename int to integerPierre Roux
2020-09-11[refman] Rename numeral to numberPierre Roux
2020-09-11[refman] Rename num to naturalPierre Roux
2020-08-03More documentation on grammars and parsingJim Fehrle
2020-07-17Documenting new primitive entry evaluable_ref usable for tactic notations.Hugo Herbelin
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
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-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-23Merge PR #12148: Consolidate funind documentation onto a single page.Clément Pit-Claudel
2020-04-20Remove Functional Scheme from Scheme chapter.Théo Zimmermann
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-11-06Replace "option" in doc when it refers to a flagJim 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 01:32:53 +0000