aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/conf.py
AgeCommit message (Collapse)Author
2021-01-05[doc] tell sphinxcontrib-bibtex which bibtex file to useEnrico Tassi
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-12-11Bump reference to 8.12 refman following unexpected 8.12.2 release.Théo Zimmermann
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-16[doc] add a link to v8.13Enrico Tassi
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-09-27Reduce nitpick_ignore list a little.Théo Zimmermann
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-06-05Merge PR #12397: Fix #12280: do not use xindy to avoid build failures on ↵Emilio Jesus Gallego Arias
some machines. Reviewed-by: SkySkimmer Reviewed-by: cpitclaudel
2020-06-05Adjust list of versions in version switcher.Théo Zimmermann
- Use the name 'dev' instead of 'master' because it is less cryptic. - Add the 'v8.12' branch. - Use the branch version only for active branches, and the latest patch-level release for the rest.
2020-05-26Fix #12280: do not use xindy to avoid build failures on some machines.Théo Zimmermann
2020-05-18Bump minimal versions of refman dependencies.Théo Zimmermann
Fixes #11936. Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-05-09[sphinx] Add links to other versions of the refmanClément Pit-Claudel
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-03-24Merge PR #11892: [refman] Fix caching, which was broken by the addition of ↵Théo Zimmermann
coq_config Reviewed-by: Zimmi48
2020-03-23[refman] Fix caching, which was broken by the addition of coq_configClément Pit-Claudel
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-03-19[refman] Remove workaround for sphinx-doc/sphinx#4983Clément Pit-Claudel
2020-03-19Document all the existing attributes.Théo Zimmermann
And fix documentation following the removal of the Template Check flag in #11546.
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-09Remove some productionlistsJim Fehrle
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
2020-02-19Update copyright in refman to year 2020.Théo Zimmermann
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
Update doc_grammar tool The grammar in the doc is generated semi-automatically with doc_grammar: - the grammar is automatically extracted from the mlg files - developer-prepared editing scripts *.mlg_edit modify the extracted grammar for clarity, simplicity and ordering of productions - chunks of the resulting grammar are automatically inserted into the rsts using instructions embedded in the rsts Running doc_grammar is currently a manual step. The grammar updates in the rst files have been manually reviewed.
2019-06-17Update copyright years outside of headers.Théo Zimmermann
These were found with the following command: $ git grep "1999-" | grep -v "2019"
2019-06-17Adapt change-header script to handle shebangs in addition to Emacs comments.Théo Zimmermann
Remove other types of lines before copyright headers.
2019-05-23Make progress toward #9411: reject new undefined references.Théo Zimmermann
We list preexisting undefined tokens explicitly in `doc/sphinx/conf.py` and prevent new ones from being introduced by making it a fatal warning. This list should be seen as a TODO. Once it is emptied, #9411 can be closed.
2019-05-13Merge PR #10085: Do not include unreleased changelog in released versions.Vincent Laporte
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: jfehrle Reviewed-by: vbgl
2019-05-08Define a new `is_a_released_version` variable in configure.ml.Théo Zimmermann
Use it to not include unreleased changes when building a released version.
2019-05-07Define minimum Sphinx version in conf.py.Théo Zimmermann
We set the minimum Sphinx version in conf.py to the one that we test in our CI and the one that is documented in doc/README.md. Hopefully, it will allow users with lower Sphinx verisons get better error messages.
2019-02-18Add diff rule for README.rst to dune refman-html aliasGaëtan Gilbert
We change regen_readme such that when given an argument it outputs there instead of overwriting the readme. Prompted by me noticing I forgot to regen in #9553.
2019-02-12Increase sphinx recursion limitGaëtan Gilbert
Not sure why but it seems required for future commits.
2018-12-14Turn warning on for undocumented objects. Closes #7602.Théo Zimmermann
2018-12-03Closes #9118: single backticks are made equivalent to double backticks; try ↵Théo Zimmermann
to fix all misuses.
2018-10-10Include all menu entries in the menu/short TOC so that users can viewJim Fehrle
menu options for all chapters without having to load a new chapter. Change "Introcution" title to "Introduction and Contents"
2018-09-25[doc] Change Sphinx project title back to "Coq"Clément Pit-Claudel
Use 'The Coq Reference Manual' only in LaTeX.
2018-09-20[doc] Replace app.info (deprecated in Sphinx 8.0) with logger.infoClément Pit-Claudel
2018-09-20[doc] Skip unneeded copies in copy_formatspecific_filesClément Pit-Claudel
2018-09-20[doc] Remove frames around code snippets in the LateX buildClément Pit-Claudel
2018-09-20[doc] Change the name that appears on the first page of the PDF manualClément Pit-Claudel
2018-09-20[doc] Fix some Sphinx LaTeX warnings and silence othersClément Pit-Claudel
2018-09-20[doc] Get rid of two Sphinx warningsClément Pit-Claudel
2018-09-20[doc] Include the rst and LaTeX preambles automatically in all filesClément Pit-Claudel
2018-09-20[doc] Improve rendering of Coq objects in PDF outputClément Pit-Claudel
2018-09-20[doc] Create a separate zebibliography file for the LaTeX buildClément Pit-Claudel
`.. bibliography::` puts the bibliography on its own page with its own title in LaTeX, but includes it inline without a title in HTML [1], so we need to maintain two separate copies of zebibliography.rst [1] https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#mismatch-between-output-of-html-and-latex-backends
2018-09-20[doc] Create a separate index file for the LaTeX buildClément Pit-Claudel
See https://github.com/sphinx-doc/sphinx/issues/4977 for context.
2018-09-20[doc] Adjust conf.py to allow LaTeX buildsClément Pit-Claudel
2018-06-17Add introduction and credits to the TOC.Théo Zimmermann
Move credits to its own chapter (closes #6573).
2018-06-08[doc] Disable smartquotes conversionClément Pit-Claudel
Closes GH-7742.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:58:41 +0000