11 files changed, 34 insertions, 25 deletions
diff --git a/doc/README.md b/doc/README.md
index 1461fa2e2c..3db1261656 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -88,8 +88,11 @@ Alternatively, you can use some specific targets:
 - `make doc-html`
   to produce all HTML documents
 
-- `make sphinx`
-   to produce the HTML and PDF versions of the reference manual
+- `make refman`
+  to produce the HTML and PDF versions of the reference manual
+
+- `make refman-{html,pdf}`
+  to produce only one format of the reference manual
 
 - `make stdlib`
   to produce all formats of the Coq standard library
@@ -103,12 +106,12 @@ to avoid treating Sphinx warnings as errors.  Otherwise, Sphinx quits
 upon detecting the first warning.  You can set this on the Sphinx `make`
 command line or as an environment variable:
 
-- `make sphinx SPHINXWARNERROR=0`
+- `make refman SPHINXWARNERROR=0`
 
 - ~~~
   export SPHINXWARNERROR=0
     ⋮
-  make sphinx
+  make refman
   ~~~
 
 Installation
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
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 97dabbf815..edf4e6ec9d 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -666,7 +666,9 @@ class ExampleDirective(BaseAdmonition):
 class PreambleDirective(Directive):
     r"""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::
 
@@ -693,7 +695,7 @@ class PreambleDirective(Directive):
         with open(abs_fname, encoding="utf-8") as ltx:
             latex = ltx.read()
 
-        node = make_math_node(latex, env.docname, nowrap=True)
+        node = make_math_node(latex, env.docname, nowrap=False)
         node['classes'] = ["math-preamble"]
         set_source_info(self, node)
         return [node]