| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-23 | Make 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-13 | Merge 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-08 | Define 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-07 | Define 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-18 | Add diff rule for README.rst to dune refman-html alias | Gaë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-12 | Increase sphinx recursion limit | Gaëtan Gilbert | |
| Not sure why but it seems required for future commits. | |||
| 2018-12-14 | Turn warning on for undocumented objects. Closes #7602. | Théo Zimmermann | |
| 2018-12-03 | Closes #9118: single backticks are made equivalent to double backticks; try ↵ | Théo Zimmermann | |
| to fix all misuses. | |||
| 2018-10-10 | Include all menu entries in the menu/short TOC so that users can view | Jim 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.info | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Skip unneeded copies in copy_formatspecific_files | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Remove frames around code snippets in the LateX build | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Change the name that appears on the first page of the PDF manual | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Fix some Sphinx LaTeX warnings and silence others | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Get rid of two Sphinx warnings | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Include the rst and LaTeX preambles automatically in all files | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Improve rendering of Coq objects in PDF output | Clément Pit-Claudel | |
| 2018-09-20 | [doc] Create a separate zebibliography file for the LaTeX build | Clé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 build | Clément Pit-Claudel | |
| See https://github.com/sphinx-doc/sphinx/issues/4977 for context. | |||
| 2018-09-20 | [doc] Adjust conf.py to allow LaTeX builds | Clément Pit-Claudel | |
| 2018-06-17 | Add introduction and credits to the TOC. | Théo Zimmermann | |
| Move credits to its own chapter (closes #6573). | |||
| 2018-06-08 | [doc] Disable smartquotes conversion | Clément Pit-Claudel | |
| Closes GH-7742. | |||
| 2018-05-22 | [doc] Add a setting to warn about empty Coq objects | Clément Pit-Claudel | |
| 2018-05-15 | [doc] Add a README to doc/sphinx/ | Clément Pit-Claudel | |
| The readme is auto-generated by combining introductory text with the docstrings in coqdomain.py. | |||
| 2018-03-15 | [Sphinx] Add credits | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Add introduction | Maxime Dénès | |
| I backported changes done to the LaTeX manual. | |||
| 2018-03-13 | [Sphinx] Add "edit on github" | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Update some metadata | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Read version number from configure | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Comment out metadata for unused backends | Maxime Dénès | |
| 2018-03-13 | [Sphinx] Remove information for .chm backend | Maxime Dénès | |
| 2018-03-09 | Integration of a sphinx-based documentation generator. | Maxime Dénès | |
| The original contribution is from Clément Pit-Claudel. I updated his code and integrated it with the Coq build system. Many improvements by Paul Steckler (MIT). This commit adds the infrastructure but no content. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |