diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/README.rst | 37 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 13 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 7 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 4 | ||||
| -rw-r--r-- | doc/sphinx/credits-contents.rst (renamed from doc/sphinx/credits.rst) | 0 | ||||
| -rw-r--r-- | doc/sphinx/credits-wrapper.latex.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/credits.html.rst (renamed from doc/sphinx/credits-wrapper.html.rst) | 2 | ||||
| -rw-r--r-- | doc/sphinx/credits.latex.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/index.html.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/index.latex.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/introduction.rst | 5 |
11 files changed, 45 insertions, 50 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index c1f3f7b4d0..4ad952bdfb 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -114,32 +114,23 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica Raised if :n:`@tactic` does not fully solve the goal. -``.. flag::`` :black_nib: A Coq flag (i.e a binary-valued setting). +``.. flag::`` :black_nib: A Coq flag (i.e. a boolean setting). Example:: .. flag:: Nonrecursive Elimination Schemes - This option controls whether types declared with the keywords - :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the + Controls whether types declared with the keywords + :cmd:`Variant` and :cmd:`Record` get an automatic declaration of induction principles. -``.. opt::`` :black_nib: A Coq option (with a string or numeric value; use "flag" for binary options) +``.. opt::`` :black_nib: A Coq option (a setting with non-boolean value, e.g. a string or numeric value). Example:: - .. opt:: Printing Width @num - :name: Printing Width + .. opt:: Hyps Limit @num + :name Hyps Limit - This command sets which left-aligned part of the width of the screen is used - for display. At the time of writing this documentation, the default value - is 78. - -``.. table::`` :black_nib: A Coq table (i.e a setting whose value is a set). - Example:: - - .. table:: Search Blacklist @string - :name: Search Blacklist - - This table controls ... + Controls the maximum number of hypotheses displayed in goals after + application of a tactic. ``.. prodn::`` A grammar production. This is useful if you intend to document individual grammar productions. @@ -159,6 +150,14 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica .. prodn:: term += let: @pattern := @term in @term .. prodn:: occ_switch ::= { {? + %| - } {* @num } } +``.. table::`` :black_nib: A Coq table, i.e. a setting that is a set of values. + Example:: + + .. table:: Search Blacklist @string + :name: Search Blacklist + + Controls ... + ``.. tacn::`` :black_nib: A tactic, or a tactic notation. Example:: @@ -293,7 +292,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo \WTEG{\forall~x:T,U}{\Prop} ``.. preamble::`` A reST directive to include a TeX file. - Mostly useful to let MathJax know about `\def`s and `\newcommand`s. + Mostly useful to let MathJax know about `\def`s and `\newcommand`s. The + contents of the TeX file are wrapped in a math environment, as MathJax + doesn't process LaTeX definitions otherwise. Usage:: diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index d03a31c044..3b9760f586 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -112,11 +112,11 @@ and checked to be :math:`-1`. .. tacn:: lia :name: lia -This tactic offers an alternative to the :tacn:`omega` and :tacn:`romega` -tactics. Roughly speaking, the deductive power of lia is the combined deductive -power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear -goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following -so-called *omega nightmare* :cite:`TheOmegaPaper`. + This tactic offers an alternative to the :tacn:`omega` tactic. Roughly + speaking, the deductive power of lia is the combined deductive power of + :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear goals + that :tacn:`omega` does not solve, such as the following so-called *omega + nightmare* :cite:`TheOmegaPaper`. .. coqtop:: in @@ -124,8 +124,7 @@ so-called *omega nightmare* :cite:`TheOmegaPaper`. 27 <= 11 * x + 13 * y <= 45 -> -10 <= 7 * x - 9 * y <= 4 -> False. -The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` and -:tacn:`romega` is under evaluation. +The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` is under evaluation. High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 828505b850..03d4f148e3 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -23,13 +23,6 @@ Description of ``omega`` If the tactic cannot solve the goal, it fails with an error message. In any case, the computation eventually stops. -.. tacv:: romega - :name: romega - - .. deprecated:: 8.9 - - Use :tacn:`lia` instead. - Arithmetical goals recognized by ``omega`` ------------------------------------------ diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index b43d5fb6f0..71f01cbb17 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -106,7 +106,7 @@ def setup(app): master_doc = "index" # General information about the project. -project = 'The Coq Reference Manual' +project = 'Coq' copyright = '1999-2018, Inria' author = 'The Coq Development Team' @@ -335,7 +335,7 @@ latex_additional_files = [ "_static/coqnotations.sty" ] -latex_documents = [('index', 'CoqRefMan.tex', project, author, 'manual')] +latex_documents = [('index', 'CoqRefMan.tex', 'The Coq Reference Manual', author, 'manual')] # The name of an image file (relative to this directory) to place at the top of # the title page. diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits-contents.rst index 212f0a65b0..212f0a65b0 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits-contents.rst diff --git a/doc/sphinx/credits-wrapper.latex.rst b/doc/sphinx/credits-wrapper.latex.rst deleted file mode 100644 index 9f7dd49af8..0000000000 --- a/doc/sphinx/credits-wrapper.latex.rst +++ /dev/null @@ -1,3 +0,0 @@ -.. _credits: - -.. include:: credits.rst diff --git a/doc/sphinx/credits-wrapper.html.rst b/doc/sphinx/credits.html.rst index 2d35a12dc2..0b2b1c6ad1 100644 --- a/doc/sphinx/credits-wrapper.html.rst +++ b/doc/sphinx/credits.html.rst @@ -4,4 +4,4 @@ Credits ------- -.. include:: credits.rst +.. include:: credits-contents.rst diff --git a/doc/sphinx/credits.latex.rst b/doc/sphinx/credits.latex.rst new file mode 100644 index 0000000000..39101f9d52 --- /dev/null +++ b/doc/sphinx/credits.latex.rst @@ -0,0 +1,3 @@ +.. _credits: + +.. include:: credits-contents.rst diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst index 9d90857061..cf12b57414 100644 --- a/doc/sphinx/index.html.rst +++ b/doc/sphinx/index.html.rst @@ -1,11 +1,8 @@ -========================== - The Coq Reference Manual -========================== - .. _introduction: +========================== Introduction ------------- +========================== .. include:: introduction.rst @@ -28,7 +25,7 @@ Table of contents :caption: Preamble self - credits-wrapper + credits .. toctree:: :caption: The language @@ -89,3 +86,8 @@ License ------- .. include:: license.rst + +.. [#PG] Proof-General is available at https://proofgeneral.github.io/. + Optionally, you can enhance it with the minor mode + Company-Coq :cite:`Pit16` + (see https://github.com/cpitclaudel/company-coq). diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst index 0f2f7b4897..af757f8746 100644 --- a/doc/sphinx/index.latex.rst +++ b/doc/sphinx/index.latex.rst @@ -7,10 +7,15 @@ Introduction .. include:: introduction.rst +.. [#PG] Proof-General is available at https://proofgeneral.github.io/. + Optionally, you can enhance it with the minor mode + Company-Coq :cite:`Pit16` + (see https://github.com/cpitclaudel/company-coq). + Credits ------- -.. include:: credits-wrapper.rst +.. include:: credits.rst License ------- diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index b8d2f6b6dc..5bb7bf542c 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -35,11 +35,6 @@ are processed from a file. The `coqtop` read-eval-print-loop can also be used directly, for debugging purposes. - .. [#PG] Proof-General is available at https://proofgeneral.github.io/. - Optionally, you can enhance it with the minor mode - Company-Coq :cite:`Pit16` - (see https://github.com/cpitclaudel/company-coq). - - The compiled mode acts as a proof checker taking a file containing a whole development in order to ensure its correctness. Moreover, |Coq|’s compiler provides an output file containing a compact |