aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/Reference-Manual.tex
Commit message (Collapse)AuthorAge
* [Sphinx] Move chapter 29 to new infrastructureGravatar Maxime Dénès2018-04-11
|
* [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] 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
|
* Port ssr manual to Coq's latex/hevea styleGravatar Enrico Tassi2017-08-02
| | | | Work done by Assia Mahboubi and Enrico Tassi
* Farewell decl_modeGravatar Enrico Tassi2017-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" environmentGravatar Matej Kosik2015-12-10
|
* ENH: examples for 'strict positivity' were expandedGravatar Matej Kosik2015-12-10
|
* Improve the table of content of the reference manual.Gravatar Guillaume Melquiond2015-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.Gravatar Guillaume Melquiond2015-04-02
|
* Separate index for vernacular options.Gravatar Maxime Dénès2015-02-17
|
* Add section numbering to the refman PDF. (Fix for bug #2365)Gravatar Guillaume Melquiond2015-02-10
|
* refman: switch all source files to utf8Gravatar Pierre Letouzey2014-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.Gravatar Matthieu Sozeau2014-07-24
|
* Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)Gravatar Guillaume Melquiond2014-04-28
|
* refman: fist stab at Asynchronous ProofsGravatar Enrico Tassi2014-01-05
|
* Documentation of the Derive plugin.Gravatar Arnaud Spiwack2013-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 StructuresGravatar Enrico Tassi2013-11-29
|
* Port rewrites of tactic documentation from branch 8.4.Gravatar gmelquio2012-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_exampleGravatar aspiwack2012-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.Gravatar aspiwack2012-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15160 85f007b7-540e-0410-9357-904b9bb8a0f7