Merge PR #8549: Fix issues introduced by the PDF manual merge

14 files changed, 51 insertions, 39 deletions

diff --git a/.gitignore b/.gitignore
index 582a8f43c7..0ab6e25852 100644
--- a/.gitignore
+++ b/.gitignore
@@ -101,7 +101,7 @@ doc/faq/axioms.pdf_t
 doc/faq/axioms.png
 doc/sphinx/index.rst
 doc/sphinx/zebibliography.rst
-doc/sphinx/credits-wrapper.rst
+doc/sphinx/credits.rst
 doc/stdlib/Library.out
 doc/stdlib/Library.ps
 doc/stdlib/Library.coqdoc.tex
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 15fcdf371a..1fb44ccbbe 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -112,7 +112,7 @@ after_script:
     - not-a-real-job
   script:
     - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/" COQBOOT=no'
-    - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= sphinx
+    - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= refman
     - make install-doc-sphinx
   artifacts:
     name: "$CI_JOB_NAME"
diff --git a/Makefile.doc b/Makefile.doc
index 788e4e61e7..db52607612 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -50,32 +50,35 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
 ######################################################################
 
 .PHONY: doc doc-html doc-pdf doc-ps
-.PHONY: stdlib full-stdlib
+.PHONY: stdlib full-stdlib sphinx
 
-doc: sphinx stdlib
+doc: refman stdlib
 
 ifndef QUICK
 SPHINX_DEPS := coq
 endif
 
-# sphinx-html and sphinx-latex
-sphinx-%: $(SPHINX_DEPS)
+# refman-html and refman-latex
+refman-%: $(SPHINX_DEPS)
 	$(SHOW)'SPHINXBUILD doc/sphinx ($*)'
 	$(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \
 		$(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$*
 
-sphinx-pdf: sphinx-latex
+refman-pdf: refman-latex
 	+$(MAKE) -C $(SPHINXBUILDDIR)/latex
 
-sphinx: $(SPHINX_DEPS)
-	+$(MAKE) sphinx-html
-	+$(MAKE) sphinx-pdf
+refman: $(SPHINX_DEPS)
+	+$(MAKE) refman-html
+	+$(MAKE) refman-pdf
+
+# compatibility alias
+sphinx: refman-html
 
 doc-html:\
-  doc/stdlib/html/index.html sphinx-html
+  doc/stdlib/html/index.html refman-html
 
 doc-pdf:\
-  doc/stdlib/Library.pdf sphinx-pdf
+  doc/stdlib/Library.pdf refman-pdf
 
 doc-ps:\
   doc/stdlib/Library.ps
@@ -188,7 +191,7 @@ install-doc-meta:
 	$(MKDIR) $(FULLDOCDIR)
 	$(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc
 
-install-doc-html: install-doc-stdlib-html install-doc-sphinx-html
+install-doc-html: install-doc-stdlib-html install-doc-sphinx
 
 install-doc-stdlib-html:
 	$(MKDIR) $(FULLDOCDIR)/html/stdlib
@@ -199,7 +202,7 @@ install-doc-printable:
 	$(INSTALLLIB) doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf
 	$(INSTALLLIB) doc/stdlib/Library.ps $(FULLDOCDIR)/ps
 
-install-doc-sphinx-html:
+install-doc-sphinx:
 	$(MKDIR) $(FULLDOCDIR)/sphinx
 	(for f in `cd doc/sphinx/_build; find . -type f`; do \
 		$(MKDIR) $$(dirname $(FULLDOCDIR)/sphinx/$$f);\
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]