aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/user-extensions/syntax-extensions.rst
AgeCommit message (Expand)Author
2021-04-23Merge PR #13965: [abbreviation] user syntax to set interp scope of argumentPierre-Marie Pédrot
2021-04-08Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular.Pierre-Marie Pédrot
2021-04-07[abbreviation] allow the user to set arguments scopeEnrico Tassi
2021-03-10Merge PR #13840: [notation] option to fine tune printing of literalscoqbot-app[bot]
2021-03-04[doc] Set/Unset Printing Raw LiteralsEnrico Tassi
2021-02-27Remove decimal-only number notationsPierre Roux
2021-02-26Signed primitive integersAna
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-12-14Merge PR #13613: [changes] mark #12765 as experimentalcoqbot-app[bot]
2020-12-11Merge PR #13519: Better primitive type support in custom string and numeral n...coqbot-app[bot]
2020-12-11[changes] mark #12765 as experimentalEnrico Tassi
2020-12-07Merge PR #13556: Fix spelling in warning entrycoqbot-app[bot]
2020-12-06Fix spelling in warning entrySimon Friis Vindum
2020-12-05Merge PR #13553: Document Number Notation for primitive integerscoqbot-app[bot]
2020-12-04Better primitive type support in custom string and numeral notations.Fabian Kunze
2020-12-03Add an anchor in syntax-extensionsMatthieu Sozeau
2020-12-02Document Number Notation for primitive integersPierre Roux
2020-11-22Updating doc wrt addition of grammar subentry "name" and deprecation of "ident".Hugo Herbelin
2020-11-20Documentation of the support for general single binders in notations.Hugo Herbelin
2020-11-19Merge PR #12984: [printing] Order notations by matching precision first, and ...coqbot-app[bot]
2020-11-18Ref. man.: showing the x ⪯ y ⪯ .. ⪯ z ⪯ t example of recursive notation.Hugo Herbelin
2020-11-17Documenting priority given to most recently declared/imported notations.Hugo Herbelin
2020-11-17Documenting the preference given to more precise notations at printing time.Hugo Herbelin
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
2020-11-05[refman] Add an example for number notationsPierre Roux
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2020-11-05[numeral notation] Add support for parameterized inductivesPierre Roux
2020-11-05[numeral notation] Handle implicit argumentsPierre Roux
2020-11-05[numeral notation] Document the via ... using ... optionPierre Roux
2020-10-30Renaming numnotoption into number_modifierPierre Roux
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-10-10Documenting the new only-parsing only-printing model.Hugo Herbelin
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:53:20 +0000