aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/user-extensions
AgeCommit message (Expand)Author
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-19[refman] Misc fixes (indentation, whitespace, notation syntax)Clé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
2019-01-22Remove unneeded | in productionlistsJim Fehrle
2018-12-12Fixing incorrect mention of coercions as being part of the interning phase.Hugo Herbelin
2018-12-12Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`Hugo Herbelin
2018-12-04Giving to type_scope a softer role in printing.Hugo Herbelin
2018-12-04Printing priority to most recent notation in case of non-open scopes with delim.Hugo Herbelin
2018-12-04Documentation of the rules for printing notations depending on scopes.Hugo Herbelin
2018-11-28Fix numeral notations doc by indentingJason Gross
2018-11-28Fix string notation docJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2018-11-21[sphinx] Progress towards closing #7602: remove most objects without a body.Théo Zimmermann
2018-11-19Typo: comment does not match codeOlivier Laurent
2018-10-30Credits for 8.9Matthieu Sozeau
2018-09-26Combined Scheme tests sort to use either "*" or "/\"Théo Winterhalter
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
2018-09-20[doc] Include the rst and LaTeX preambles automatically in all filesClément Pit-Claudel
2018-09-10Documenting "Declare Scope".Hugo Herbelin
2018-08-31Give a proper error message on num-not in functorJason Gross
2018-08-31[numeral notations] support aliasesJason Gross
2018-08-31Add periods in response to PR commentsJason Gross
2018-08-31Add a warning about abstract after being a no-opJason Gross
2018-08-31Update doc and test-suite after supporting univ polyJason Gross
2018-08-31Fix numeral notation for a rebase on top of masterJason Gross
2018-08-31Numeral Notation: minor text improvements suggested by J. GrossPierre Letouzey
2018-08-31Numeral Notation: some documentation in the refmanPierre Letouzey
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: direc...Zeimer
2018-08-06Merge PR #8189: Some trivial fixes to the custom entry documentation.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:43:14 +0000