aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.doc
Commit message (Collapse)AuthorAge
* [Sphinx] Move chapter 6 to new infrastructureGravatar Maxime Dénès2018-04-10
|
* [Sphinx] Move chapter 15 to new infrastructureGravatar Maxime Dénès2018-04-10
|
* [Sphinx] Move chapter 7 to new infrastructureGravatar Maxime Dénès2018-04-09
|
* [Sphinx] Move chapter 30 to new infrastructureGravatar Maxime Dénès2018-04-05
|
* [Sphinx] Move chapter 28 to new infrastructureGravatar Maxime Dénès2018-04-04
|
* [Sphinx] Move chapter 27 to new infrastructureGravatar Maxime Dénès2018-03-30
|
* [Sphinx] Move chapter 25 to new infrastructureGravatar Maxime Dénès2018-03-30
|
* [Sphinx] Move chapter 26 to new infrastructureGravatar Maxime Dénès2018-03-29
|
* [Sphinx] Move chapter 24 to new infrastructureGravatar Maxime Dénès2018-03-29
|
* [Sphinx] Move chapter 23 to new infrastructureGravatar Maxime Dénès2018-03-29
|
* [Sphinx] Move chapter 18 to new infrastructureGravatar Maxime Dénès2018-03-29
|
* Move Classes.tex to type-classes.rstGravatar Matthieu Sozeau2018-03-26
|
* Merge branch 'master' into sphinx-doc-chapter-22Gravatar Guillaume Melquiond2018-03-22
|\
| * Merge branch 'master' into sphinx-doc-chapter-21Gravatar Guillaume Melquiond2018-03-22
| |\
| | * Merge branch 'master' into sphinx-doc-chapter-19Gravatar Guillaume Melquiond2018-03-22
| | |\
* | | | [Sphinx] Move chapter 22 to new infrastructureGravatar Maxime Dénès2018-03-22
| | | |
| * | | [Sphinx] Move chapter 21 to new infrastructureGravatar Maxime Dénès2018-03-22
|/ / /
| * / [Sphinx] Move chapter 19 to new infrastructureGravatar Maxime Dénès2018-03-22
|/ /
| * [Sphinx] Move chapter 17 to new infrastructureGravatar Maxime Dénès2018-03-22
|/
* [Sphinx] Add chapter 11Gravatar Maxime Dénès2018-03-16
| | | | | Thanks to Enrico Tassi, Assia Mahboubi, Laurence Rideau and Yves Bertot for porting this chapter.
* [Sphinx] Move chapter 3 to new infrastructureGravatar Maxime Dénès2018-03-15
|
* [Sphinx] Move chapter 16 to new infrastructureGravatar Maxime Dénès2018-03-15
|
* [Sphinx] Move chapter 14 to new infrastructureGravatar Maxime Dénès2018-03-15
|
* [Sphinx] Move chapter 13 to new infrastructureGravatar Maxime Dénès2018-03-15
|
* [Sphinx] Move chapter 12 to new infrastructureGravatar Maxime Dénès2018-03-15
|
* [Sphinx] Move chapter 10 to new infrastructureGravatar Maxime Dénès2018-03-15
|
* [Sphinx] Move chapter 8 to new infrastructureGravatar Maxime Dénès2018-03-15
|
* [Sphinx] Move chapter 5 to new infrastructureGravatar Maxime Dénès2018-03-15
|
* [Sphinx] Move chapter 4 to new infrastructureGravatar Maxime Dénès2018-03-15
|
* [Sphinx] Add chapter 2Gravatar Maxime Dénès2018-03-15
| | | | Thanks to Paul Steckler for porting this chapter.
* [Sphinx] Move chapter 2 to new infrastructureGravatar Maxime Dénès2018-03-15
|
* [Sphinx] Move credits to new infrastructureGravatar Maxime Dénès2018-03-15
|
* [Sphinx] Move introduction to new infrastructureGravatar Maxime Dénès2018-03-13
|
* Integration of a sphinx-based documentation generator.Gravatar Maxime Dénès2018-03-09
| | | | | | | | 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.
* Remove NOPLUGINDOCS optionGravatar mrmr19932018-03-05
|
* Build docs for plugins by default, add NOPLUGINDOCS flag to disableGravatar mrmr19932018-03-05
|
* Tidy up ml-doc outut, give it a separate output directoryGravatar mrmr19932018-03-05
|
* Use computed deps to generate ml-doc and use implicit mli-doc depsGravatar mrmr19932018-03-05
|
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |
* | Use relative path for show_latex_messagesGravatar mrmr19932018-02-27
| |
* | Use MYCAMLP5LIB instead of undefined MYCAMLP4LIBGravatar mrmr19932018-02-27
|/ | | | | This completes the work of b60906cc3ee3f994babf9cceff2971bd03485f2f
* [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
| | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
* Removing the FAQ, which has been moved to the GitHub wiki for thisGravatar Matt Quinn2017-12-18
| | | | repository. Also removing FAQ-related build rules.
* Remove some unused parts of the reference manual.Gravatar Guillaume Melquiond2017-09-22
|
* Merge PR #979: Fix install-doc target and other gitlab failuresGravatar Maxime Dénès2017-09-15
|\
| * Fix install-doc targetGravatar Gaëtan Gilbert2017-08-31
| | | | | | | | | | | | Since 8995d0857277019b54c24672439d3e19b2fcb5af [make doc] puts css files in subdirectories of doc/refman/html. These subdirectories cause a failure when doing [install doc/refman/html/* target].
* | [general] Merge parsing with highparsing, put toplevel at the top of the ↵Gravatar Emilio Jesus Gallego Arias2017-08-29
|/ | | | linking chain.
* Port ssr manual to Coq's latex/hevea styleGravatar Enrico Tassi2017-08-02
| | | | Work done by Assia Mahboubi and Enrico Tassi
* Makefile.doc: implement serve-refman-8080 targetGravatar Enrico Tassi2017-08-02
| | | | | | We make it so that, by default, the HTML reference manual looks like the one published online (same .css) and we provide a target to serve it locally (requires python).