aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/user-extensions
AgeCommit message (Expand)Author
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
2018-03-15[Sphinx] Add chapter 13Maxime Dénès
2018-03-15[Sphinx] Move chapter 13 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Add chapter 12Maxime Dénès
2018-03-15[Sphinx] Move chapter 12 to new infrastructureMaxime Dénès