diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/README.rst | 37 | ||||
| -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 |
9 files changed, 39 insertions, 36 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/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 |