| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-10-02 | [doc] [api] Remove `ocamldoc` support in favor of `odoc` | Emilio Jesus Gallego Arias | |
| This PR removes support for `ocamldoc` in favor of `odoc`. Following a recent discussion in OCaml's discord, it turns out that basically all the ecosystem has migrated to odoc, thus we follow suit and may focus on `odoc` for Coq's ML API documentation. | |||
| 2018-09-25 | Fix Sphinx manual targets. | Théo Zimmermann | |
| New targets refman, refman-html and refman-pdf. sphinx keeps its previous meaning (compatibility alias for refman-html). install-doc-sphinx has been accidentally renamed. | |||
| 2018-09-20 | Fix race condition. | Théo Zimmermann | |
| 2018-09-20 | [doc] Add sphinx-html, sphinx-latex, and sphinx-pdf targets | Clément Pit-Claudel | |
| 2018-09-03 | [doc] Build ML API documentation artifact. | Emilio Jesus Gallego Arias | |
| This is not optimal for we have to rebuild the `.cmi` as `ocamldoc` cannot yet use the `_install_ci/` directory. Overall the `mli` documentation is in a sorry state, however, I think this is a first step in order to improve it. Note that the `ml-doc` target seems broken in OCaml 4.07.0, needs investigation. cc: #7155 | |||
| 2018-08-29 | Create SPHINXWARNERROR variable that controls whether the Sphinx | Jim Fehrle | |
| "treat errors as warnings" flag (-W) is applied. "1" or undefined includes the flag, other values or undefined omit it. Removed the "-warn-error" parameter to configure. "-profile XXX" will no longer cause these flags to be used. | |||
| 2018-06-08 | gitlab: build sphinx doc in separate job | Gaëtan Gilbert | |
| 2018-05-22 | [doc] Fix an incorrect use of $PWD in Makefile.doc | Clément Pit-Claudel | |
| 2018-05-12 | Sphinx: a "QUICK=1" option to bypass recompilation of the library. | Hugo Herbelin | |
| 2018-05-10 | Clean-up in Makefile.doc and include Sphinx in doc-html target. | Théo Zimmermann | |
| 2018-05-10 | Remove tutorials. | Théo Zimmermann | |
| 2018-04-28 | [doc] Remove unused dependencies. | Emilio Jesus Gallego Arias | |
| AFAICS `imagemagick` `hacha` and `transfig` are not used anymore. | |||
| 2018-04-16 | Remove LaTeX refman, now that migration to Sphinx is complete | Maxime Dénès | |
| 2018-04-14 | [Sphinx] Build with warnings as errors | Maxime Dénès | |
| Most of these warnings should really be errors (ill-formed input, invalid cross references, etc.) so we make it the default. | |||
| 2018-04-14 | [Sphinx] Move chapter 9 to new infrastructure. | Théo Zimmermann | |
| 2018-04-13 | [Sphinx] Move chapter 1 to new infrastructure | Maxime Dénès | |
| 2018-04-11 | [Sphinx] Move chapter 29 to new infrastructure | Maxime Dénès | |
| 2018-04-10 | [Sphinx] Move chapter 6 to new infrastructure | Maxime Dénès | |
| 2018-04-10 | [Sphinx] Move chapter 15 to new infrastructure | Maxime Dénès | |
| 2018-04-09 | [Sphinx] Move chapter 7 to new infrastructure | Maxime Dénès | |
| 2018-04-05 | [Sphinx] Move chapter 30 to new infrastructure | Maxime Dénès | |
| 2018-04-04 | [Sphinx] Move chapter 28 to new infrastructure | Maxime Dénès | |
| 2018-03-30 | [Sphinx] Move chapter 27 to new infrastructure | Maxime Dénès | |
| 2018-03-30 | [Sphinx] Move chapter 25 to new infrastructure | Maxime Dénès | |
| 2018-03-29 | [Sphinx] Move chapter 26 to new infrastructure | Maxime Dénès | |
| 2018-03-29 | [Sphinx] Move chapter 24 to new infrastructure | Maxime Dénès | |
| 2018-03-29 | [Sphinx] Move chapter 23 to new infrastructure | Maxime Dénès | |
| 2018-03-29 | [Sphinx] Move chapter 18 to new infrastructure | Maxime Dénès | |
| 2018-03-26 | Move Classes.tex to type-classes.rst | Matthieu Sozeau | |
| 2018-03-22 | Merge branch 'master' into sphinx-doc-chapter-22 | Guillaume Melquiond | |
| 2018-03-22 | Merge branch 'master' into sphinx-doc-chapter-21 | Guillaume Melquiond | |
| 2018-03-22 | Merge branch 'master' into sphinx-doc-chapter-19 | Guillaume Melquiond | |
| 2018-03-22 | [Sphinx] Move chapter 22 to new infrastructure | Maxime Dénès | |
| 2018-03-22 | [Sphinx] Move chapter 21 to new infrastructure | Maxime Dénès | |
| 2018-03-22 | [Sphinx] Move chapter 19 to new infrastructure | Maxime Dénès | |
| 2018-03-22 | [Sphinx] Move chapter 17 to new infrastructure | Maxime Dénès | |
| 2018-03-16 | [Sphinx] Add chapter 11 | Maxime Dénès | |
| Thanks to Enrico Tassi, Assia Mahboubi, Laurence Rideau and Yves Bertot for porting this chapter. | |||
| 2018-03-15 | [Sphinx] Move chapter 3 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 16 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 14 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 13 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 12 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 10 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 8 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 5 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move chapter 4 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Add chapter 2 | Maxime Dénès | |
| Thanks to Paul Steckler for porting this chapter. | |||
| 2018-03-15 | [Sphinx] Move chapter 2 to new infrastructure | Maxime Dénès | |
| 2018-03-15 | [Sphinx] Move credits to new infrastructure | Maxime Dénès | |
