aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/user-extensions
AgeCommit message (Expand)Author
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
2018-08-04Merge PR #8142: Improved the grammar and spelling of chapter 'Syntax extensio...Théo Zimmermann
2018-08-04Improved the grammar and spelling of chapter 'Syntax extensions and interpret...Zeimer
2018-08-02Merge PR #8143: Improved grammar and spelling in chapters 'Proof Schemes' and...Théo Zimmermann
2018-08-01Improved grammar and spelling in chapters 'Proof Schemes' and 'The Coq comman...Zeimer
2018-07-31Camlp{4 => 5}Jason Gross
2018-07-31Fix doc for no associativityJason Gross
2018-07-30Some trivial fixes to the custom entry documentation.Théo Zimmermann
2018-07-29Miscellaneous uniformization of typography in chapter syntax extensions.Hugo Herbelin
2018-07-29Documenting custom entries in the reference manual + CHANGES.Hugo Herbelin
2018-06-30doc: typesetting and hyperlinks in Syntax ExtensionsLysxia
2018-05-15[doc] Small fixesClément Pit-Claudel
2018-05-09[sphinx] Fix new warnings related to tacn, cmd, opt...Théo Zimmermann
2018-05-05[sphinx] Fix a hardcoded reference.Théo Zimmermann
2018-04-16[Sphinx] Clean-up indicesMaxime Dénès
2018-04-14[Sphinx] Fix all remaining warnings.Maxime Dénès
2018-04-14[sphinx] Fix many warnings.Théo Zimmermann
2018-04-09Translation fixes in chapter syntax extensions.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:14:36 +0000