Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | [Sphinx] Move chapter 29 to new infrastructure | Maxime Dénès | 2018-04-11 |
| | |||
* | [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-10 |
| | |||
* | [Sphinx] Move chapter 7 to new infrastructure | Maxime Dénès | 2018-04-09 |
| | |||
* | [Sphinx] Move chapter 30 to new infrastructure | Maxime Dénès | 2018-04-05 |
| | |||
* | [Sphinx] Move chapter 28 to new infrastructure | Maxime Dénès | 2018-04-04 |
| | |||
* | [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-30 |
| | |||
* | [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-29 |
| | |||
* | Move Classes.tex to type-classes.rst | Matthieu Sozeau | 2018-03-26 |
| | |||
* | 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-22 |
|/ | |||
* | [Sphinx] Add chapter 11 | Maxime Dénès | 2018-03-16 |
| | | | | | Thanks to Enrico Tassi, Assia Mahboubi, Laurence Rideau and Yves Bertot for porting this chapter. | ||
* | [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] 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-15 |
| | |||
* | [Sphinx] Move introduction to new infrastructure | Maxime Dénès | 2018-03-13 |
| | |||
* | Port ssr manual to Coq's latex/hevea style | Enrico Tassi | 2017-08-02 |
| | | | | Work done by Assia Mahboubi and Enrico Tassi | ||
* | Farewell decl_mode | Enrico Tassi | 2017-03-07 |
| | | | | | This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests. | ||
* | CLEANUP: putting examples inside "figure" environment | Matej Kosik | 2015-12-10 |
| | |||
* | ENH: examples for 'strict positivity' were expanded | Matej Kosik | 2015-12-10 |
| | |||
* | Improve the table of content of the reference manual. | Guillaume Melquiond | 2015-07-31 |
| | | | | | Also remove AsyncProofs.tex from the list of preprocessed files, as it is doubtful it will ever contains Coq scripts. | ||
* | Make sure that hyperref creates the proper links to the documentation indexes. | Guillaume Melquiond | 2015-04-02 |
| | |||
* | Separate index for vernacular options. | Maxime Dénès | 2015-02-17 |
| | |||
* | Add section numbering to the refman PDF. (Fix for bug #2365) | Guillaume Melquiond | 2015-02-10 |
| | |||
* | refman: switch all source files to utf8 | Pierre Letouzey | 2014-12-09 |
| | | | | | | Putting utf8 everywhere helps the maintainance of the online refman. And anyway, this is the way to go. We should also chase and migrate the few remaining iso-latin-1 files elsewhere in the sources. | ||
* | Start documenting universe polymorphism. | Matthieu Sozeau | 2014-07-24 |
| | |||
* | Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964) | Guillaume Melquiond | 2014-04-28 |
| | |||
* | refman: fist stab at Asynchronous Proofs | Enrico Tassi | 2014-01-05 |
| | |||
* | Documentation of the Derive plugin. | Arnaud Spiwack | 2013-12-04 |
| | | | I put it in a new chapter of the Addendum of the manual. Which is meant to be dedicated to plugins with short documentation. | ||
* | First stab at documenting Canonical Structures | Enrico Tassi | 2013-11-29 |
| | |||
* | Port rewrites of tactic documentation from branch 8.4. | gmelquio | 2012-09-15 |
| | | | | | | | | This encompasses commits r15183, r15190, r15243, r15262, r15276, r15277, r15278, r15337. The merge did not go without troubles, but hopefully none of the changes were lost in process. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15806 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
* | Addedum to documentation of bullets: I now use the dedicated coq_example | aspiwack | 2012-05-10 |
| | | | | | | environment to display the example. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15295 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
* | Restores pdf bookmarks in the reference manual. | aspiwack | 2012-04-13 |
| | | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15160 85f007b7-540e-0410-9357-904b9bb8a0f7 |