| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2018-03-13 | [Sphinx] Move introduction to new infrastructure | 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. | |||
| 2018-03-05 | Remove NOPLUGINDOCS option | mrmr1993 | |
| 2018-03-05 | Build docs for plugins by default, add NOPLUGINDOCS flag to disable | mrmr1993 | |
| 2018-03-05 | Tidy up ml-doc outut, give it a separate output directory | mrmr1993 | |
| 2018-03-05 | Use computed deps to generate ml-doc and use implicit mli-doc deps | mrmr1993 | |
| 2018-03-05 | Merge PR #6855: Update headers following #6543. | Maxime Dénès | |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann | |
| 2018-02-27 | Use relative path for show_latex_messages | mrmr1993 | |
| 2018-02-27 | Use MYCAMLP5LIB instead of undefined MYCAMLP4LIB | mrmr1993 | |
| This completes the work of b60906cc3ee3f994babf9cceff2971bd03485f2f | |||
| 2017-12-27 | [API] remove large file containing duplicate interfaces | Enrico Tassi | |
| ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client. | |||
| 2017-12-18 | Removing the FAQ, which has been moved to the GitHub wiki for this | Matt Quinn | |
| repository. Also removing FAQ-related build rules. | |||
| 2017-09-22 | Remove some unused parts of the reference manual. | Guillaume Melquiond | |
| 2017-09-15 | Merge PR #979: Fix install-doc target and other gitlab failures | Maxime Dénès | |
| 2017-08-31 | Fix install-doc target | Gaëtan Gilbert | |
| 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]. | |||
| 2017-08-29 | [general] Merge parsing with highparsing, put toplevel at the top of the ↵ | Emilio Jesus Gallego Arias | |
| linking chain. | |||
| 2017-08-02 | Port ssr manual to Coq's latex/hevea style | Enrico Tassi | |
| Work done by Assia Mahboubi and Enrico Tassi | |||
| 2017-08-02 | Makefile.doc: implement serve-refman-8080 target | Enrico Tassi | |
| 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). | |||
| 2017-06-07 | Put all plugins behind an "API". | Matej Kosik | |
| 2017-05-28 | Gitlab CI | Gaëtan Gilbert | |
| 2017-03-07 | Farewell decl_mode | Enrico Tassi | |
| This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests. | |||
| 2016-12-19 | Avoid concurrent runs when producing html documentation (bug #5269). | Guillaume Melquiond | |
| Make does not allow for rules that produce multiple outputs (unless they are pattern rules). As a consequence, the hacha rule could be run several times concurrently, thus causing doc/refman/html to be deleted under the feet of some runs. This commit fixes the issue by turning the rule into a single-output rule and adding a dummy rule to handle all the other indexes. Note that this is not a perfect solution since, if the user were to manually delete one of the auxiliary index, it would not be rebuilt until the main index is. | |||
| 2016-10-21 | Merge remote-tracking branch 'gforge/v8.5' into v8.6 | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/Makefile.doc