aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum
AgeCommit message (Expand)Author
2018-08-02Merge PR #8176: Improved grammar and spelling in chapters 'Type Classes', 'Om...Théo Zimmermann
2018-08-01Added a tactic index entry for nsatz, reformatted commands in chapter 'Genera...Zeimer
2018-08-01Improved grammar and spelling in the remaining chapters of the Reference Manual.Zeimer
2018-08-01Improved grammar and spelling in chapter 'Extended pattern matching' of the R...Zeimer
2018-08-01Improved grammar and spelling in chapters 'Type Classes', 'Omega' and 'Microm...Zeimer
2018-08-01Merge PR #8192: Fix typos and typesetting of doc on ProgramThéo Zimmermann
2018-08-01Merge PR #8184: Improved grammar and spelling in chapters 'Extraction', 'Prog...Théo Zimmermann
2018-07-30Fix typos and typesetting of doc on ProgramLysxia
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
2018-07-29Improved grammar and spelling in chapters 'Extraction', 'Program' and 'ring a...Zeimer
2018-07-26Improved chapters 'Implicit Coercions' and 'Canonical Structures' of the Refe...Zeimer
2018-07-17Remove fourier pluginMaxime Dénès
2018-06-25Merge PR #7559: Existing Class noop when already a class + warning.Matthieu Sozeau
2018-06-19[doc] Use productionlist instead of prodn in ring.rstClément Pit-Claudel
2018-06-13doc: fix typo.whitequark
2018-06-08Existing Class noop when already a class + warning.Gaëtan Gilbert
2018-05-16Typo in documentation of DeriveJoachim Breitner
2018-05-15[doc] Address feedback on doc writer guideClément Pit-Claudel
2018-05-15[doc] Small fixesClément Pit-Claudel
2018-05-14Merge PR #7374: [sphinx] More fatal warnings.Maxime Dénès
2018-05-09[sphinx] Improvements around the Show commands, including missing indices and...Théo Zimmermann
2018-05-09[sphinx] Fix new warnings related to tacn, cmd, opt...Théo Zimmermann
2018-05-05[sphinx] Improve typeclass chapter.Théo Zimmermann
2018-05-05[sphinx] Re-indent to get much better rendering.Théo Zimmermann
2018-05-05Two more uses of verbatim in doc.Théo Zimmermann
2018-05-05Clean-up around cmd documentation.Théo Zimmermann
2018-05-05Add some refs in the Omega chapter.Théo Zimmermann
2018-05-05More fixes in the Generalized Rewriting chapter.Théo Zimmermann
2018-05-05[sphinx] More use of cmd references in Extraction chapter.Théo Zimmermann
2018-05-05Fix error messages and make them consistent.Théo Zimmermann
2018-05-05Clean-up around options.Théo Zimmermann
2018-05-05Fix failing example in refman.Théo Zimmermann
2018-05-05[sphinx] Fix some references.Théo Zimmermann
2018-05-05[sphinx] Use option direct reference.Théo Zimmermann
2018-05-05Fix typo in Coercions chapter.Théo Zimmermann
2018-04-16[Sphinx] Clean-up indicesMaxime Dénès
2018-04-16[Sphinx] Fix a lot of references and description of optionsMaxime 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-13Merge PR #7117: Sphinx doc chapter 29Théo Zimmermann
2018-04-12[Sphinx] Add chapter 29Maxime Dénès
2018-04-11[sphinx] Remove migration artefacts.Théo Zimmermann
2018-04-11[Sphinx] Move chapter 29 to new infrastructureMaxime Dénès
2018-04-05[Sphinx] Add chapter 30Maxime Dénès
2018-04-05[Sphinx] Move chapter 30 to new infrastructureMaxime Dénès
2018-04-04[Sphinx] Add chapter 28Maxime Dénès
2018-04-04[Sphinx] Move chapter 28 to new infrastructureMaxime Dénès
2018-03-30[Sphinx] Add chapter 27Maxime Dénès
2018-03-30[Sphinx] Move chapter 27 to new infrastructureMaxime Dénès
2018-03-30[Sphinx] Add chapter 25Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:45:09 +0000