aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/README.rst
AgeCommit message (Expand)Author
2018-08-31Merge PR #8170: Don't index names starting with `_` in docsThéo Zimmermann
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
2018-07-25[sphinx] Add a way of skipping names in the indexes.Théo Zimmermann
2018-06-19[doc] Rewrite and document the prodn directiveClément Pit-Claudel
2018-05-25[doc] Allow more than one signature and name per Sphinx objectClément Pit-Claudel
2018-05-22[doc] Document the new report_undocumented_coq_objects settingClément Pit-Claudel
2018-05-22[doc] Add a list of common mistakesClément Pit-Claudel
2018-05-15[doc] More feedback on doc writer guideClément Pit-Claudel
2018-05-15[doc] Address feedback on doc writer guideClément Pit-Claudel
2018-05-15[doc] Add an ELisp snippet to insert Sphinx roles and quotesClément Pit-Claudel
2018-05-15[doc] Add a README to doc/sphinx/Clément Pit-Claudel