aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/user-extensions
AgeCommit message (Expand)Author
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-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ...coqbot-app[bot]
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-27Reduce nitpick_ignore list a little.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 16:45:51 +0000