diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/README.rst | 4 | ||||
| -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, 23 insertions, 19 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 904945a58d..4ad952bdfb 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -292,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 |