aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/Reference-Manual.tex
AgeCommit message (Collapse)Author
2018-04-16Remove LaTeX refman, now that migration to Sphinx is completeMaxime Dénès
2018-04-13[Sphinx] Move chapter 1 to new infrastructureMaxime Dénès
2018-04-11[Sphinx] Move chapter 29 to new infrastructureMaxime Dénès
2018-04-10[Sphinx] Move chapter 6 to new infrastructureMaxime Dénès
2018-04-10[Sphinx] Move chapter 15 to new infrastructureMaxime Dénès
2018-04-09[Sphinx] Move chapter 7 to new infrastructureMaxime Dénès
2018-04-05[Sphinx] Move chapter 30 to new infrastructureMaxime Dénès
2018-04-04[Sphinx] Move chapter 28 to new infrastructureMaxime Dénès
2018-03-30[Sphinx] Move chapter 27 to new infrastructureMaxime Dénès
2018-03-30[Sphinx] Move chapter 25 to new infrastructureMaxime Dénès
2018-03-29[Sphinx] Move chapter 26 to new infrastructureMaxime Dénès
2018-03-29[Sphinx] Move chapter 24 to new infrastructureMaxime Dénès
2018-03-29[Sphinx] Move chapter 23 to new infrastructureMaxime Dénès
2018-03-29[Sphinx] Move chapter 18 to new infrastructureMaxime Dénès
2018-03-26Move Classes.tex to type-classes.rstMatthieu Sozeau
2018-03-22Merge branch 'master' into sphinx-doc-chapter-22Guillaume Melquiond
2018-03-22Merge branch 'master' into sphinx-doc-chapter-21Guillaume Melquiond
2018-03-22Merge branch 'master' into sphinx-doc-chapter-19Guillaume Melquiond
2018-03-22[Sphinx] Move chapter 22 to new infrastructureMaxime Dénès
2018-03-22[Sphinx] Move chapter 21 to new infrastructureMaxime Dénès
2018-03-22[Sphinx] Move chapter 19 to new infrastructureMaxime Dénès
2018-03-22[Sphinx] Move chapter 17 to new infrastructureMaxime Dénès
2018-03-16[Sphinx] Add chapter 11Maxime 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 infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 16 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 14 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 13 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 12 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 10 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 8 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 5 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 4 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move chapter 2 to new infrastructureMaxime Dénès
2018-03-15[Sphinx] Move credits to new infrastructureMaxime Dénès
2018-03-13[Sphinx] Move introduction to new infrastructureMaxime Dénès
2017-08-02Port ssr manual to Coq's latex/hevea styleEnrico Tassi
Work done by Assia Mahboubi and Enrico Tassi
2017-03-07Farewell decl_modeEnrico Tassi
This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests.
2015-12-10CLEANUP: putting examples inside "figure" environmentMatej Kosik
2015-12-10ENH: examples for 'strict positivity' were expandedMatej Kosik
2015-07-31Improve the table of content of the reference manual.Guillaume Melquiond
Also remove AsyncProofs.tex from the list of preprocessed files, as it is doubtful it will ever contains Coq scripts.
2015-04-02Make sure that hyperref creates the proper links to the documentation indexes.Guillaume Melquiond
2015-02-17Separate index for vernacular options.Maxime Dénès
2015-02-10Add section numbering to the refman PDF. (Fix for bug #2365)Guillaume Melquiond
2014-12-09refman: switch all source files to utf8Pierre Letouzey
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.
2014-07-24Start documenting universe polymorphism.Matthieu Sozeau
2014-04-28Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)Guillaume Melquiond
2014-01-05refman: fist stab at Asynchronous ProofsEnrico Tassi
2013-12-04Documentation of the Derive plugin.Arnaud Spiwack
I put it in a new chapter of the Addendum of the manual. Which is meant to be dedicated to plugins with short documentation.
2013-11-29First stab at documenting Canonical StructuresEnrico Tassi
2012-09-15Port rewrites of tactic documentation from branch 8.4.gmelquio
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