Merge PR #8418: Add a PDF version of the manual

55 files changed, 714 insertions, 345 deletions

diff --git a/.gitignore b/.gitignore
index 8fc3c802ad..582a8f43c7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -99,6 +99,9 @@ doc/faq/axioms.eps
 doc/faq/axioms.eps_t
 doc/faq/axioms.pdf_t
 doc/faq/axioms.png
+doc/sphinx/index.rst
+doc/sphinx/zebibliography.rst
+doc/sphinx/credits-wrapper.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 0115ac9eff..27d7fbf243 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -9,7 +9,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2018-09-05-V1"
+  CACHEKEY: "bionic_coq-V2018-09-20-V2"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
diff --git a/.travis.yml b/.travis.yml
index dd28410bec..766c76c29c 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -105,8 +105,8 @@ matrix:
     # Full Coq test-suite with two compilers
     - if: NOT (type = pull_request)
       env:
-      - TEST_TARGET="test-suite"
-      - EXTRA_CONF="-coqide opt -with-doc yes"
+      - TEST_TARGET="doc-html test-suite"
+      - EXTRA_CONF="-coqide opt"
       - EXTRA_OPAM="${LABLGTK} ounit"
       before_install: &sphinx-install
       - sudo pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex
@@ -119,26 +119,17 @@ matrix:
           - aspcud
           - libgtk2.0-dev
           - libgtksourceview2.0-dev
-          - texlive-latex-base
-          - texlive-latex-recommended
-          - texlive-latex-extra
-          - texlive-math-extra
-          - texlive-fonts-recommended
-          - texlive-fonts-extra
-          - latex-xcolor
-          - ghostscript
-          - tipa
           - python3
           - python3-pip
           - python3-setuptools
 
     - if: NOT (type = pull_request)
       env:
-      - TEST_TARGET="test-suite"
+      - TEST_TARGET="doc-html test-suite"
       - COMPILER="${COMPILER_BE}"
       - FINDLIB_VER="${FINDLIB_VER_BE}"
       - CAMLP5_VER="${CAMLP5_VER_BE}"
-      - EXTRA_CONF="-coqide opt -with-doc yes"
+      - EXTRA_CONF="-coqide opt"
       - EXTRA_OPAM="${LABLGTK_BE} ounit"
       before_install: *sphinx-install
       addons:
@@ -150,11 +141,11 @@ matrix:
     # Full test-suite with flambda
     - if: NOT (type = pull_request)
       env:
-      - TEST_TARGET="test-suite"
+      - TEST_TARGET="doc-html test-suite"
       - COMPILER="${COMPILER_BE}+flambda"
       - FINDLIB_VER="${FINDLIB_VER_BE}"
       - CAMLP5_VER="${CAMLP5_VER_BE}"
-      - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3"
+      - EXTRA_CONF="-coqide opt -flambda-opts -O3"
       - EXTRA_OPAM="${LABLGTK_BE} ounit"
       before_install: *sphinx-install
       addons:
diff --git a/CHANGES b/CHANGES
index 1bf0e0edd4..453d82758a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -215,6 +215,10 @@ Notations
 Changes from 8.8.1 to 8.8.2
 ===========================
 
+Documentation
+
+- A PDF version of the reference manual is available once again.
+
 Tools
 
 - The coq-makefile targets `print-pretty-timed`, `print-pretty-timed-diff`,
diff --git a/Makefile.doc b/Makefile.doc
index 0dcf9daf27..788e4e61e7 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -58,17 +58,24 @@ ifndef QUICK
 SPHINX_DEPS := coq
 endif
 
+# sphinx-html and sphinx-latex
+sphinx-%: $(SPHINX_DEPS)
+	$(SHOW)'SPHINXBUILD doc/sphinx ($*)'
+	$(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \
+		$(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$*
+
+sphinx-pdf: sphinx-latex
+	+$(MAKE) -C $(SPHINXBUILDDIR)/latex
+
 sphinx: $(SPHINX_DEPS)
-	$(SHOW)'SPHINXBUILD doc/sphinx'
-	$(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html
-	@echo
-	@echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html."
+	+$(MAKE) sphinx-html
+	+$(MAKE) sphinx-pdf
 
 doc-html:\
-  doc/stdlib/html/index.html sphinx
+  doc/stdlib/html/index.html sphinx-html
 
 doc-pdf:\
-  doc/stdlib/Library.pdf
+  doc/stdlib/Library.pdf sphinx-pdf
 
 doc-ps:\
   doc/stdlib/Library.ps
@@ -181,7 +188,7 @@ install-doc-meta:
 	$(MKDIR) $(FULLDOCDIR)
 	$(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc
 
-install-doc-html: install-doc-stdlib-html install-doc-sphinx
+install-doc-html: install-doc-stdlib-html install-doc-sphinx-html
 
 install-doc-stdlib-html:
 	$(MKDIR) $(FULLDOCDIR)/html/stdlib
@@ -192,7 +199,7 @@ install-doc-printable:
 	$(INSTALLLIB) doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf
 	$(INSTALLLIB) doc/stdlib/Library.ps $(FULLDOCDIR)/ps
 
-install-doc-sphinx:
+install-doc-sphinx-html:
 	$(MKDIR) $(FULLDOCDIR)/sphinx
 	(for f in `cd doc/sphinx/_build; find . -type f`; do \
 		$(MKDIR) $$(dirname $(FULLDOCDIR)/sphinx/$$f);\
diff --git a/default.nix b/default.nix
index 6f759f41d1..88992a30a3 100644
--- a/default.nix
+++ b/default.nix
@@ -23,8 +23,8 @@
 
 { pkgs ?
     (import (fetchTarball {
-      url = "https://github.com/NixOS/nixpkgs/archive/4477cf04b6779a537cdb5f0bd3dd30e75aeb4a3b.tar.gz";
-      sha256 = "1i39wsfwkvj9yryj8di3jibpdg3b3j86ych7s9rb6z79k08yaaxc";
+      url = "https://github.com/NixOS/nixpkgs/archive/947ae71dcec680b5075ece14e38eae64831b9819.tar.gz";
+      sha256 = "15nryymfch4fzxk6nacli4gw4cyicpdjwzai5v3bc0azaslww2x5";
     }) {})
 , ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06
 , buildIde ? true
@@ -38,18 +38,6 @@
 with pkgs;
 with stdenv.lib;
 
-let dune =
-  overrideDerivation jbuilder (o: {
-    name = "dune-1.1.1";
-    src = fetchFromGitHub {
-      owner = "ocaml";
-      repo = "dune";
-      rev = "1.1.1";
-      sha256 = "0v2pnxpmqsvrvidpwxvbsypzhqfdnjs5crjp9y61qi8nyj8d75zw";
-    };
-  });
-in
-
 stdenv.mkDerivation rec {
 
   name = "coq";
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 8b26294d8f..9fad274bf4 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-09-05-V1"
+# CACHEKEY: "bionic_coq-V2018-09-20-V2"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -7,13 +7,19 @@ LABEL maintainer="e@x80.org"
 ENV DEBIAN_FRONTEND="noninteractive"
 
 RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
+        # Dependencies of the image, the test-suite and external projects
         m4 automake autoconf time wget rsync git gcc-multilib opam \
+        # Dependencies of lablgtk (for CoqIDE)
         libgtk2.0-dev libgtksourceview2.0-dev \
-        texlive-latex-extra texlive-fonts-recommended texlive-science tipa \
-        python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex \
-        python3-setuptools python3-wheel python3-pip
-
-RUN pip3 install antlr4-python3-runtime
+        # Dependencies of stdlib and sphinx doc
+        texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
+        xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \
+        # Dependencies of source-doc and coq-makefile
+        texlive-science tipa
+
+# More dependencies of the sphinx doc
+RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \
+                 antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0
 
 # Basic OPAM setup
 ENV NJOBS="2" \
diff --git a/doc/README.md b/doc/README.md
index 47507de52d..cb3427e010 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -28,18 +28,18 @@ To produce the complete documentation in HTML, you will need Coq dependencies
 listed in [`INSTALL`](../INSTALL). Additionally, the Sphinx-based
 reference manual requires Python 3, and the following Python packages:
 
-    sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex
+  - sphinx >= 1.7.8
+  - sphinx_rtd_theme >= 0.2.5b2
+  - beautifulsoup4 >= 4.0.6
+  - antlr4-python3-runtime >= 4.7.1
+  - pexpect >= 4.2.1
+  - sphinxcontrib-bibtex >= 0.4.0
 
-You can install them using `pip3 install` or using your distribution's package
-manager. E.g. under recent Debian-based operating systems (Debian 10 "Buster",
-Ubuntu 18.04, ...) you can use:
+To install them, you should first install pip and setuptools (for instance,
+with `apt install python3-pip python3-setuptools` on Debian / Ubuntu) then run:
 
-    apt install python3-sphinx python3-pexpect python3-sphinx-rtd-theme \
-                python3-bs4 python3-sphinxcontrib.bibtex python3-pip
-
-Then, install the missing Python3 Antlr4 package:
-
-    pip3 install antlr4-python3-runtime
+    pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime \
+                 pexpect sphinxcontrib-bibtex
 
 Nix users should get the correct development environment to build the
 HTML documentation from Coq's [`default.nix`](../default.nix) (note this
@@ -54,10 +54,19 @@ additional tools are required:
   - pdflatex
   - dvips
   - makeindex
+  - xelatex
+  - latexmk
+  - xindy
+
+All of them are part of the TexLive distribution. E.g. on Debian / Ubuntu,
+install them with:
+
+    apt install texlive-full
 
-Install them using your package manager. E.g. on Debian / Ubuntu:
+Or if you want to use less disk space:
 
-    apt install texlive-latex-extra texlive-fonts-recommended
+    apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \
+                latexmk xindy
 
 Compilation
 -----------
@@ -80,7 +89,7 @@ Alternatively, you can use some specific targets:
   to produce all HTML documents
 
 - `make sphinx`
-   to produce the HTML version of the reference manual
+   to produce the HTML and PDF versions of the reference manual
 
 - `make stdlib`
   to produce all formats of the Coq standard library
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 4673107e3d..369a3a0db8 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -260,8 +260,8 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
 
        .. inference:: name
 
-          newline-separated premisses
-          ------------------------
+          newline-separated premises
+          --------------------------
           conclusion
 
     Example::
@@ -274,14 +274,12 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
           -----------------------------
           \WTEG{\forall~x:T,U}{\Prop}
 
-``.. preamble::`` A reST directive for hidden math.
-    Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s.
+``.. preamble::`` A reST directive to include a TeX file.
+    Mostly useful to let MathJax know about `\def`s and `\newcommand`s.
 
-    Example::
-
-       .. preamble::
+    Usage::
 
-          \newcommand{\paren}[#1]{\left(#1\right)}
+       .. preamble:: preamble.tex
 
 Coq roles
 =========
@@ -364,6 +362,32 @@ DON'T
 
      This is equivalent to ``Axiom`` :token`ident` : :token:`term`.
 
+..
+
+DO
+  .. code::
+
+     :n:`power_tac @term [@ltac]`
+       allows :tacn:`ring` and :tacn:`ring_simplify` to recognize …
+
+DON'T
+  .. code::
+
+     power_tac :n:`@term` [:n:`@ltac`]
+       allows :tacn:`ring` and :tacn:`ring_simplify` to recognize …
+
+..
+
+DO
+  .. code::
+
+     :n:`name={*; attr}`
+
+DON'T
+  .. code::
+
+     ``name=``:n:`{*; attr}`
+
 Omitting annotations
 --------------------
 
@@ -377,6 +401,86 @@ DON'T
 
      .. tacv:: assert form as intro_pattern
 
+Using the ``.. coqtop::`` directive for syntax highlighting
+-----------------------------------------------------------
+
+DO
+  .. code::
+
+     A tactic of the form:
+
+     .. coqdoc::
+
+        do [ t1 | … | tn ].
+
+     is equivalent to the standard Ltac expression:
+
+     .. coqdoc::
+
+        first [ t1 | … | tn ].
+
+DON'T
+  .. code::
+
+     A tactic of the form:
+
+     .. coqtop:: in
+
+        do [ t1 | … | tn ].
+
+     is equivalent to the standard Ltac expression:
+
+     .. coqtop:: in
+
+        first [ t1 | … | tn ].
+
+Overusing plain quotes
+----------------------
+
+DO
+  .. code::
+
+     The :tacn:`refine` tactic can raise the :exn:`Invalid argument` exception.
+     The term :g:`let a = 1 in a a` is ill-typed.
+
+DON'T
+  .. code::
+
+     The ``refine`` tactic can raise the ``Invalid argument`` exception.
+     The term ``let a = 1 in a a`` is ill-typed.
+
+Plain quotes produce plain text, without highlighting or cross-references.
+
+Overusing the ``example`` directive
+-----------------------------------
+
+DO
+  .. code::
+
+     Here is a useful axiom:
+
+     .. coqdoc::
+
+        Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
+
+DO
+  .. code::
+
+     .. example:: Using proof-irrelevance
+
+        If you assume the axiom above, …
+
+DON'T
+  .. code::
+
+     Here is a useful axiom:
+
+     .. example::
+
+        .. coqdoc::
+
+           Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
+
 Tips and tricks
 ===============
 
@@ -398,7 +502,7 @@ Add either ``undo`` to the first block or ``reset`` to the second block to avoid
 Abbreviations and macros
 ------------------------
 
-Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual.  Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_.
+Substitutions for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_.  This file is automatically included in all manual pages.
 
 Emacs
 -----
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index c333d6e9d5..86914a71df 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -140,6 +140,32 @@ DON'T
 
      This is equivalent to ``Axiom`` :token`ident` : :token:`term`.
 
+..
+
+DO
+  .. code::
+
+     :n:`power_tac @term [@ltac]`
+       allows :tacn:`ring` and :tacn:`ring_simplify` to recognize …
+
+DON'T
+  .. code::
+
+     power_tac :n:`@term` [:n:`@ltac`]
+       allows :tacn:`ring` and :tacn:`ring_simplify` to recognize …
+
+..
+
+DO
+  .. code::
+
+     :n:`name={*; attr}`
+
+DON'T
+  .. code::
+
+     ``name=``:n:`{*; attr}`
+
 Omitting annotations
 --------------------
 
@@ -153,6 +179,86 @@ DON'T
 
      .. tacv:: assert form as intro_pattern
 
+Using the ``.. coqtop::`` directive for syntax highlighting
+-----------------------------------------------------------
+
+DO
+  .. code::
+
+     A tactic of the form:
+
+     .. coqdoc::
+
+        do [ t1 | … | tn ].
+
+     is equivalent to the standard Ltac expression:
+
+     .. coqdoc::
+
+        first [ t1 | … | tn ].
+
+DON'T
+  .. code::
+
+     A tactic of the form:
+
+     .. coqtop:: in
+
+        do [ t1 | … | tn ].
+
+     is equivalent to the standard Ltac expression:
+
+     .. coqtop:: in
+
+        first [ t1 | … | tn ].
+
+Overusing plain quotes
+----------------------
+
+DO
+  .. code::
+
+     The :tacn:`refine` tactic can raise the :exn:`Invalid argument` exception.
+     The term :g:`let a = 1 in a a` is ill-typed.
+
+DON'T
+  .. code::
+
+     The ``refine`` tactic can raise the ``Invalid argument`` exception.
+     The term ``let a = 1 in a a`` is ill-typed.
+
+Plain quotes produce plain text, without highlighting or cross-references.
+
+Overusing the ``example`` directive
+-----------------------------------
+
+DO
+  .. code::
+
+     Here is a useful axiom:
+
+     .. coqdoc::
+
+        Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
+
+DO
+  .. code::
+
+     .. example:: Using proof-irrelevance
+
+        If you assume the axiom above, …
+
+DON'T
+  .. code::
+
+     Here is a useful axiom:
+
+     .. example::
+
+        .. coqdoc::
+
+           Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
+
 Tips and tricks
 ===============
 
@@ -174,7 +280,7 @@ Add either ``undo`` to the first block or ``reset`` to the second block to avoid
 Abbreviations and macros
 ------------------------
 
-Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual.  Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_.
+Substitutions for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``), along with some useful LaTeX macros, are defined in a `separate file </doc/sphinx/refman-preamble.rst>`_.  This file is automatically included in all manual pages.
 
 Emacs
 -----
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
index 2cc1f95c08..3e414a714c 100644
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -1,4 +1,3 @@
-.. include:: ../replaces.rst
 .. _canonicalstructures:
 
 Canonical Structures
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index e507a224c6..ad6a06d2b0 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _extendedpatternmatching:
 
 Extended pattern-matching
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index e3d25cf5cf..4bfa45d54c 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _extraction:
 
 Extraction of programs in |OCaml| and Haskell
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index e0babb6c4e..403b163196 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -1,6 +1,3 @@
-.. include:: ../preamble.rst
-.. include:: ../replaces.rst
-
 .. _generalizedrewriting:
 
 Generalized rewriting
@@ -126,10 +123,10 @@ parameters is any term :math:`f \, t_1 \ldots t_n`.
 
    .. coqtop:: in
 
-     forall (A : Type) (S1 S1’ S2 S2’ : list A),
-       set_eq A S1 S1’ ->
-       set_eq A S2 S2’ ->
-       set_eq A (union A S1 S2) (union A S1’ S2’).
+     forall (A: Type) (S1 S1' S2 S2': list A),
+       set_eq A S1 S1' ->
+       set_eq A S2 S2' ->
+       set_eq A (union A S1 S2) (union A S1' S2').
 
    The signature of the function ``union A`` is ``set_eq A ==> set_eq A ==> set_eq A``
    for all ``A``.
@@ -451,7 +448,7 @@ various combinations of properties on relations and morphisms are
 represented as records and instances of theses classes are put in a
 hint database. For example, the declaration:
 
-.. coqtop:: in
+.. coqdoc::
 
    Add Parametric Relation (x1 : T1) ... (xn : Tn) : (A t1 ... tn) (Aeq t′1 ... t′m)
      [reflexivity proved by refl]
@@ -462,7 +459,7 @@ hint database. For example, the declaration:
 
 is equivalent to an instance declaration:
 
-.. coqtop:: in
+.. coqdoc::
 
    Instance (x1 : T1) ... (xn : Tn) => id : @Equivalence (A t1 ... tn) (Aeq t′1 ... t′m) :=
      [Equivalence_Reflexive := refl]
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 23cbd76eda..5cb0eaf469 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _implicitcoercions:
 
 Implicit Coercions
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
index 0f2d35d044..2cde65dcdc 100644
--- a/doc/sphinx/addendum/miscellaneous-extensions.rst
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _miscellaneousextensions:
 
 Miscellaneous extensions
diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst
index 9adeca46fc..e7a8c238ac 100644
--- a/doc/sphinx/addendum/nsatz.rst
+++ b/doc/sphinx/addendum/nsatz.rst
@@ -1,5 +1,3 @@
-.. include:: ../preamble.rst
-
 .. _nsatz_chapter:
 
 Nsatz: tactics for proving equalities in integral domains
diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst
index 8ee8f52227..eb19d57203 100644
--- a/doc/sphinx/addendum/parallel-proof-processing.rst
+++ b/doc/sphinx/addendum/parallel-proof-processing.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _asynchronousandparallelproofprocessing:
 
 Asynchronous and Parallel Proof Processing
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index d6895f5fe5..24247f7bb1 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -1,6 +1,3 @@
-.. include:: ../preamble.rst
-.. include:: ../replaces.rst
-
 .. this should be just "_program", but refs to it don't work
 
 .. _programs:
@@ -378,6 +375,3 @@ Frequently Asked Questions
        using lazy evaluation;
     #. Mutual recursion on the underlying inductive type isn’t possible
        anymore, but nested mutual recursion is always possible.
-
-.. bibliography:: ../biblio.bib
-   :keyprefix: p-
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 8cb86e2267..58617916c0 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -1,11 +1,9 @@
-.. include:: ../replaces.rst
 .. |ra| replace:: :math:`\rightarrow_{\beta\delta\iota}`
 .. |la| replace:: :math:`\leftarrow_{\beta\delta\iota}`
 .. |eq| replace:: `=`:sub:`(by the main correctness theorem)`
 .. |re| replace:: ``(PEeval`` `v` `ap`\ ``)``
 .. |le| replace:: ``(Pphi_dev`` `v` ``(norm`` `ap`\ ``))``
 
-
 .. _theringandfieldtacticfamilies:
 
 The ring and field tactic families
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index ab4b4a9824..418014809f 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _typeclasses:
 
 Type Classes
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 7e77dea457..706ce1065c 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _polymorphicuniverses:
 
 Polymorphic Universes
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index c74d8f540c..aa8537c92d 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -121,7 +121,7 @@ s},
     volume = {7998},
     editor = {Sandrine Blazy and Christine Paulin and David Pichardie },
     series = {LNCS },
-    doi = {10.1007/978-3-642-39634-2\_5 },
+    doi = {10.1007/978-3-642-39634-2_5},
     year = {2013},
 }
 
@@ -136,7 +136,7 @@ s},
   pages       = {85--95},
   month       = {November},
   year        = {2000},
-  url         = {http://www.lirmm.fr/\%7Edelahaye/papers/ltac\%20(LPAR\%2700).pdf}
+  url         = {http://www.lirmm.fr/%7Edelahaye/papers/ltac%20(LPAR%2700).pdf}
 }
 
 @Article{Dyc92,
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 8127d3df3f..b43d5fb6f0 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -24,6 +24,8 @@
 
 import sys
 import os
+from shutil import copyfile
+import sphinx
 
 # Increase recursion limit for sphinx
 sys.setrecursionlimit(1500)
@@ -36,6 +38,12 @@ sys.path.append(os.path.abspath('../../config/'))
 
 import coq_config
 
+# -- Prolog ---------------------------------------------------------------
+
+# Include substitution definitions in all files
+with open("refman-preamble.rst") as s:
+    rst_prolog = s.read()
+
 # -- General configuration ------------------------------------------------
 
 # If your documentation needs a minimal Sphinx version, state it here.
@@ -66,11 +74,39 @@ source_suffix = '.rst'
 # The encoding of source files.
 #source_encoding = 'utf-8-sig'
 
+# Add extra cases here to support more formats
+
+SUPPORTED_FORMATS = ["html", "latex"]
+
+def readbin(fname):
+    try:
+        with open(fname, mode="rb") as f:
+            return f.read()
+    except FileNotFoundError:
+        return None
+
+def copy_formatspecific_files(app):
+    ext = ".{}.rst".format(app.builder.name)
+    for fname in sorted(os.listdir(app.srcdir)):
+        if fname.endswith(ext):
+            src = os.path.join(app.srcdir, fname)
+            dst = os.path.join(app.srcdir, fname[:-len(ext)] + ".rst")
+            logger = sphinx.util.logging.getLogger(__name__)
+            if readbin(src) == readbin(dst):
+                logger.info("Skipping {}: {} is up to date".format(src, dst))
+            else:
+                logger.info("Copying {} to {}".format(src, dst))
+                copyfile(src, dst)
+
+def setup(app):
+    app.connect('builder-inited', copy_formatspecific_files)
+
 # The master toctree document.
-master_doc = 'index'
+# We create this file in `copy_master_doc` above.
+master_doc = "index"
 
 # General information about the project.
-project = 'Coq'
+project = 'The Coq Reference Manual'
 copyright = '1999-2018, Inria'
 author = 'The Coq Development Team'
 
@@ -104,9 +140,10 @@ exclude_patterns = [
     'Thumbs.db',
     '.DS_Store',
     'introduction.rst',
+    'refman-preamble.rst',
     'README.rst',
     'README.template.rst'
-]
+] + ["*.{}.rst".format(fmt) for fmt in SUPPORTED_FORMATS]
 
 # The reST default role (used for this markup: `text`) to use for all
 # documents.
@@ -129,6 +166,7 @@ primary_domain = 'coq'
 # The name of the Pygments (syntax highlighting) style to use.
 pygments_style = 'sphinx'
 highlight_language = 'text'
+suppress_warnings = ["misc.highlighting_failure"]
 
 # A list of ignored prefixes for module index sorting.
 #modindex_common_prefix = []
@@ -257,57 +295,57 @@ smartquotes = False
 ###########################
 # Set things up for XeTeX #
 ###########################
+
 latex_elements = {
     'babel': '',
     'fontenc': '',
     'inputenc': '',
     'utf8extra': '',
     'cmappkg': '',
-    # https://www.topbug.net/blog/2015/12/10/a-collection-of-issues-about-the-latex-output-in-sphinx-and-the-solutions/
     'papersize': 'letterpaper',
     'classoptions': ',openany', # No blank pages
-    'polyglossia' : '\\usepackage{polyglossia}',
-    'unicode-math' : '\\usepackage{unicode-math}',
-    'microtype' : '\\usepackage{microtype}',
-    "preamble": r"\usepackage{coqnotations}"
+    'polyglossia': '\\usepackage{polyglossia}',
+    'sphinxsetup': 'verbatimwithframe=false',
+    'preamble': r"""
+                 \usepackage{unicode-math}
+                 \usepackage{microtype}
+
+                 % Macro definitions
+                 \usepackage{refman-preamble}
+
+                 % Style definitions for notations
+                 \usepackage{coqnotations}
+
+                 % Style tweaks
+                 \newcssclass{sigannot}{\textrm{#1:}}
+
+                 % Silence 'LaTeX Warning: Command \nobreakspace invalid in math mode'
+                 \everymath{\def\nobreakspace{\ }}
+                 """
 }
 
-from sphinx.builders.latex import LaTeXBuilder
+latex_engine = "xelatex"
 
 ########
 # done #
 ########
 
-latex_additional_files = ["_static/coqnotations.sty"]
+latex_additional_files = [
+    "refman-preamble.sty",
+    "_static/coqnotations.sty"
+]
 
-# Grouping the document tree into LaTeX files. List of tuples
-# (source start file, target name, title,
-#  author, documentclass [howto, manual, or own class]).
-# latex_documents = [
-#    (master_doc, 'CoqRefMan.tex', 'Coq Documentation',
-#     'The Coq Development Team', 'manual'),
-#]
+latex_documents = [('index', 'CoqRefMan.tex', project, author, 'manual')]
 
 # The name of an image file (relative to this directory) to place at the top of
 # the title page.
-#latex_logo = None
-
-# For "manual" documents, if this is true, then toplevel headings are parts,
-# not chapters.
-#latex_use_parts = False
+# latex_logo = "../../ide/coq.png"
 
 # If true, show page references after internal links.
 #latex_show_pagerefs = False
 
 # If true, show URL addresses after external links.
-#latex_show_urls = False
-
-# Documents to append as an appendix to all manuals.
-#latex_appendices = []
-
-# If false, no module index is generated.
-#latex_domain_indices = True
-
+latex_show_urls = 'footnote'
 
 # -- Options for manual page output ---------------------------------------
 
diff --git a/doc/sphinx/coq-cmdindex.rst b/doc/sphinx/coq-cmdindex.rst
index 7df6cb36c5..fd0b342ae4 100644
--- a/doc/sphinx/coq-cmdindex.rst
+++ b/doc/sphinx/coq-cmdindex.rst
@@ -1,3 +1,5 @@
+:orphan:
+
 .. hack to get index in TOC
 
 -----------------
diff --git a/doc/sphinx/coq-exnindex.rst b/doc/sphinx/coq-exnindex.rst
index 100c57b085..dbf60bb06c 100644
--- a/doc/sphinx/coq-exnindex.rst
+++ b/doc/sphinx/coq-exnindex.rst
@@ -1,3 +1,5 @@
+:orphan:
+
 .. hack to get index in TOC
 
 ----------------------
diff --git a/doc/sphinx/coq-optindex.rst b/doc/sphinx/coq-optindex.rst
index f8046a800b..925d4cd185 100644
--- a/doc/sphinx/coq-optindex.rst
+++ b/doc/sphinx/coq-optindex.rst
@@ -1,3 +1,5 @@
+:orphan:
+
 .. hack to get index in TOC
 
 -----------------
diff --git a/doc/sphinx/coq-tacindex.rst b/doc/sphinx/coq-tacindex.rst
index 588104f465..31b2f7f8cb 100644
--- a/doc/sphinx/coq-tacindex.rst
+++ b/doc/sphinx/coq-tacindex.rst
@@ -1,3 +1,5 @@
+:orphan:
+
 .. hack to get index in TOC
 
 -------------
diff --git a/doc/sphinx/credits-wrapper.html.rst b/doc/sphinx/credits-wrapper.html.rst
new file mode 100644
index 0000000000..2d35a12dc2
--- /dev/null
+++ b/doc/sphinx/credits-wrapper.html.rst
@@ -0,0 +1,7 @@
+.. _credits:
+
+-------
+Credits
+-------
+
+.. include:: credits.rst
diff --git a/doc/sphinx/credits-wrapper.latex.rst b/doc/sphinx/credits-wrapper.latex.rst
new file mode 100644
index 0000000000..9f7dd49af8
--- /dev/null
+++ b/doc/sphinx/credits-wrapper.latex.rst
@@ -0,0 +1,3 @@
+.. _credits:
+
+.. include:: credits.rst
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index be0b5d5f12..be6fe5704e 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits.rst
@@ -1,12 +1,3 @@
-.. include:: preamble.rst
-.. include:: replaces.rst
-
-.. _credits:
-
--------------------------------------------
-Credits
--------------------------------------------
-
 Coq is a proof assistant for higher-order logic, allowing the
 development of computer programs consistent with their formal
 specification. It is the result of about ten years of research of the
diff --git a/doc/sphinx/genindex.rst b/doc/sphinx/genindex.rst
index a991c7f9f8..29f792b3aa 100644
--- a/doc/sphinx/genindex.rst
+++ b/doc/sphinx/genindex.rst
@@ -1,3 +1,5 @@
+:orphan:
+
 .. hack to get index in TOC
 
 -----
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.html.rst
index baf2e0d981..9d90857061 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.html.rst
@@ -1,11 +1,16 @@
-.. include:: preamble.rst
-.. include:: replaces.rst
+==========================
+ The Coq Reference Manual
+==========================
+
+.. _introduction:
+
+Introduction
+------------
 
 .. include:: introduction.rst
 
-------------------
 Table of contents
-------------------
+-----------------
 
 .. toctree::
    :caption: Indexes
@@ -23,7 +28,7 @@ Table of contents
    :caption: Preamble
 
    self
-   credits
+   credits-wrapper
 
 .. toctree::
    :caption: The language
@@ -80,12 +85,7 @@ Table of contents
 
    zebibliography
 
-This material (the Coq Reference Manual) may be distributed only subject to the
-terms and conditions set forth in the Open Publication License, v1.0 or later
-(the latest version is presently available at
-http://www.opencontent.org/openpub). Options A and B are not elected.
+License
+-------
 
-.. [#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).
+.. include:: license.rst
diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst
new file mode 100644
index 0000000000..0f2f7b4897
--- /dev/null
+++ b/doc/sphinx/index.latex.rst
@@ -0,0 +1,81 @@
+==========================
+ The Coq Reference Manual
+==========================
+
+Introduction
+------------
+
+.. include:: introduction.rst
+
+Credits
+-------
+
+.. include:: credits-wrapper.rst
+
+License
+-------
+
+.. include:: license.rst
+
+The language
+------------
+
+.. toctree::
+
+   language/gallina-specification-language
+   language/gallina-extensions
+   language/coq-library
+   language/cic
+   language/module-system
+
+The proof engine
+----------------
+
+.. toctree::
+
+   proof-engine/vernacular-commands
+   proof-engine/proof-handling
+   proof-engine/tactics
+   proof-engine/ltac
+   proof-engine/detailed-tactic-examples
+   proof-engine/ssreflect-proof-language
+
+User extensions
+---------------
+
+.. toctree::
+
+   user-extensions/syntax-extensions
+   user-extensions/proof-schemes
+
+Practical tools
+---------------
+
+.. toctree::
+
+   practical-tools/coq-commands
+   practical-tools/utilities
+   practical-tools/coqide
+
+Addendum
+--------
+
+.. toctree::
+
+   addendum/extended-pattern-matching
+   addendum/implicit-coercions
+   addendum/canonical-structures
+   addendum/type-classes
+   addendum/omega
+   addendum/micromega
+   addendum/extraction
+   addendum/program
+   addendum/ring
+   addendum/nsatz
+   addendum/generalized-rewriting
+   addendum/parallel-proof-processing
+   addendum/miscellaneous-extensions
+   addendum/universe-polymorphism
+
+.. toctree::
+   zebibliography
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index b57e4b209c..b8d2f6b6dc 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -1,9 +1,3 @@
-.. _introduction:
-
-------------------------
-Introduction
-------------------------
-
 This document is the Reference Manual of the |Coq| proof assistant.
 To start using Coq, it is advised to first read a tutorial.
 Links to several tutorials can be found at
@@ -41,6 +35,11 @@ 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/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index ac0f0f8ea6..c8c3e37efb 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1,6 +1,3 @@
-.. include:: ../preamble.rst
-.. include:: ../replaces.rst
-
 .. _calculusofinductiveconstructions:
 
 
@@ -1010,7 +1007,7 @@ the Type hierarchy.
 
    It is possible to declare the same inductive definition in the
    universe :math:`\Type`. The :g:`exType` inductive definition has type
-   :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT_intro}`
+   :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT}_{\kw{intro}}`
    has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`.
 
    .. coqtop:: all
@@ -1264,14 +1261,14 @@ The |Coq| term for this proof
 will be written:
 
 .. math::
-   \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n \endkw
+   \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n \kwend
 
 In this expression, if :math:`m` eventually happens to evaluate to
 :math:`(c_i~u_1 … u_{p_i})` then the expression will behave as specified in its :math:`i`-th branch
 and it will reduce to :math:`f_i` where the :math:`x_{i1} …x_{ip_i}` are replaced by the
 :math:`u_1 … u_{p_i}` according to the ι-reduction.
 
-Actually, for type checking a :math:`\Match…\with…\endkw` expression we also need
+Actually, for type checking a :math:`\Match…\with…\kwend` expression we also need
 to know the predicate P to be proved by case analysis. In the general
 case where :math:`I` is an inductively defined :math:`n`-ary relation, :math:`P` is a predicate
 over :math:`n+1` arguments: the :math:`n` first ones correspond to the arguments of :math:`I`
@@ -1285,7 +1282,7 @@ using the syntax:
 .. math::
    \Match~m~\as~x~\In~I~\_~a~\return~P~\with~
    (c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | …
-   | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\endkw
+   | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend
    
 The :math:`\as` part can be omitted if either the result type does not depend
 on :math:`m` (non-dependent elimination) or :math:`m` is a variable (in this case, :math:`m`
@@ -1471,6 +1468,8 @@ We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math:
    where
 
    .. math::
+      :nowrap:
+
       \begin{eqnarray*}
         P & = & \lambda~l~.~P^\prime\\
         f_1 & = & t_1\\
@@ -1711,13 +1710,15 @@ for primitive recursive operators. The following reductions are now
 possible:
 
 .. math::
-   \def\plus{\mathsf{plus}}
-   \def\tri{\triangleright_\iota}
-   \begin{eqnarray*}
-   \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\
-                                  & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\
-                                  & \tri & \nS~(\nS~(\nS~\nO))\\
-   \end{eqnarray*}
+   :nowrap:
+
+   {\def\plus{\mathsf{plus}}
+    \def\tri{\triangleright_\iota}
+    \begin{eqnarray*}
+    \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\
+                                   & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\
+                                   & \tri & \nS~(\nS~(\nS~\nO))\\
+    \end{eqnarray*}}
 
 .. _Mutual-induction:
 
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 9de30e2190..320448d46e 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _thecoqlibrary:
 
 The |Coq| library
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 0fbe7ac70b..27ed176a9b 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _extensionsofgallina:
 
 Extensions of |Gallina|
@@ -22,7 +20,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
 
 .. _record_grammar:
 
-  .. productionlist:: `sentence`
+  .. productionlist:: sentence
      record         : `record_keyword` `record_body` with … with `record_body`
      record_keyword : Record | Inductive | CoInductive
      record_body    : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }.
@@ -82,11 +80,13 @@ To build an object of type :n:`@ident`, one should provide the constructor
        Definition half := mkRat true 1 2 (O_S 1) one_two_irred.
        Check half.
 
+.. FIXME: move this to the main grammar in the spec chapter
+
 .. _record-named-fields-grammar:
 
   .. productionlist::
-    term : {| [`field_def` ; … ; `field_def`] |}
-    field_def : name [binders] := `term`
+    record_term : {| [`field_def` ; … ; `field_def`] |}
+    field_def : name [binders] := `record_term`
 
 Alternatively, the following syntax allows creating objects by using named fields, as
 shown in this grammar. The fields do not have to be in any particular order, nor do they have
@@ -154,12 +154,14 @@ It can be activated for printing with
        Set Printing Projections.
        Check top half.
 
+.. FIXME: move this to the main grammar in the spec chapter
+
 .. _record_projections_grammar:
 
   .. productionlist:: terms
-     term : term `.` ( qualid )
-          : | term `.` ( qualid arg … arg )
-          : | term `.` ( @`qualid` `term` … `term` )
+     projection : projection `.` ( `qualid` )
+          : | projection `.` ( `qualid` `arg` … `arg` )
+          : | projection `.` ( @`qualid` `term` … `term` )
 
   Syntax of Record projections
 
diff --git a/doc/sphinx/language/module-system.rst b/doc/sphinx/language/module-system.rst
index e6a6736654..15fee91245 100644
--- a/doc/sphinx/language/module-system.rst
+++ b/doc/sphinx/language/module-system.rst
@@ -1,6 +1,3 @@
-.. include:: ../preamble.rst
-.. include:: ../replaces.rst
-
 .. _themodulesystem:
 
 The Module System
diff --git a/doc/sphinx/license.rst b/doc/sphinx/license.rst
new file mode 100644
index 0000000000..232b04211c
--- /dev/null
+++ b/doc/sphinx/license.rst
@@ -0,0 +1,4 @@
+This material (the Coq Reference Manual) may be distributed only subject to the
+terms and conditions set forth in the Open Publication License, v1.0 or later
+(the latest version is presently available at
+http://www.opencontent.org/openpub). Options A and B are not elected.
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 9498f37c7e..343ca9ed7d 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _thecoqcommands:
 
 The |Coq| commands
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index bc6a074a27..9455228e7d 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _coqintegrateddevelopmentenvironment:
 
 |Coq| Integrated Development Environment
@@ -263,7 +261,7 @@ for the ∀ symbol. A list of symbol codes is available at
 An alternative method which does not require to know the hexadecimal
 code of the character is to use an Input Method Editor. On POSIX
 systems (Linux distributions, BSD variants and MacOS X), you can
-use `uim` version 1.6 or later which provides a :math:`\LaTeX`-style input
+use `uim` version 1.6 or later which provides a LaTeX-style input
 method.
 
 To configure uim, execute uim-pref-gtk as your regular user. In the
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index b9a4d2a7bd..5d300c3d6d 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _utilities:
 
 ---------------------
diff --git a/doc/sphinx/preamble.rst b/doc/sphinx/preamble.rst
deleted file mode 100644
index 395f558a85..0000000000
--- a/doc/sphinx/preamble.rst
+++ /dev/null
@@ -1,92 +0,0 @@
-.. preamble::
-
-   \[
-   \newcommand{\alors}{\textsf{then}}
-   \newcommand{\alter}{\textsf{alter}}
-   \newcommand{\as}{\kw{as}}
-   \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)}
-   \newcommand{\bool}{\textsf{bool}}
-   \newcommand{\case}{\kw{case}}
-   \newcommand{\conc}{\textsf{conc}}
-   \newcommand{\cons}{\textsf{cons}}
-   \newcommand{\consf}{\textsf{consf}}
-   \newcommand{\conshl}{\textsf{cons\_hl}}
-   \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)}
-   \newcommand{\emptyf}{\textsf{emptyf}}
-   \newcommand{\End}{\kw{End}}
-   \newcommand{\endkw}{\kw{end}}
-   \newcommand{\EqSt}{\textsf{EqSt}}
-   \newcommand{\even}{\textsf{even}}
-   \newcommand{\evenO}{\textsf{even_O}}
-   \newcommand{\evenS}{\textsf{even_S}}
-   \newcommand{\false}{\textsf{false}}
-   \newcommand{\filter}{\textsf{filter}}
-   \newcommand{\Fix}{\kw{Fix}}
-   \newcommand{\fix}{\kw{fix}}
-   \newcommand{\for}{\textsf{for}}
-   \newcommand{\forest}{\textsf{forest}}
-   \newcommand{\from}{\textsf{from}}
-   \newcommand{\Functor}{\kw{Functor}}
-   \newcommand{\haslength}{\textsf{has\_length}}
-   \newcommand{\hd}{\textsf{hd}}
-   \newcommand{\ident}{\textsf{ident}}
-   \newcommand{\In}{\kw{in}}
-   \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)}
-   \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)}
-   \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)}
-   \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}}
-   \newcommand{\injective}{\kw{injective}}
-   \newcommand{\kw}[1]{\textsf{#1}}
-   \newcommand{\lb}{\lambda}
-   \newcommand{\length}{\textsf{length}}
-   \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3}
-   \newcommand{\List}{\textsf{list}}
-   \newcommand{\lra}{\longrightarrow}
-   \newcommand{\Match}{\kw{match}}
-   \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})}
-   \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})}
-   \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})}
-   \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})}
-   \newcommand{\mto}{.\;}
-   \newcommand{\Nat}{\mathbb{N}}
-   \newcommand{\nat}{\textsf{nat}}
-   \newcommand{\Nil}{\textsf{nil}}
-   \newcommand{\nilhl}{\textsf{nil\_hl}}
-   \newcommand{\nO}{\textsf{O}}
-   \newcommand{\node}{\textsf{node}}
-   \newcommand{\nS}{\textsf{S}}
-   \newcommand{\odd}{\textsf{odd}}
-   \newcommand{\oddS}{\textsf{odd_S}}
-   \newcommand{\ovl}[1]{\overline{#1}}
-   \newcommand{\Pair}{\textsf{pair}}
-   \newcommand{\Prod}{\textsf{prod}}
-   \newcommand{\Prop}{\textsf{Prop}}
-   \newcommand{\return}{\kw{return}}
-   \newcommand{\Set}{\textsf{Set}}
-   \newcommand{\si}{\textsf{if}}
-   \newcommand{\sinon}{\textsf{else}}
-   \newcommand{\Sort}{\cal S}
-   \newcommand{\Str}{\textsf{Stream}}
-   \newcommand{\Struct}{\kw{Struct}}
-   \newcommand{\subst}[3]{#1\{#2/#3\}}
-   \newcommand{\tl}{\textsf{tl}}
-   \newcommand{\tree}{\textsf{tree}}
-   \newcommand{\true}{\textsf{true}}
-   \newcommand{\Type}{\textsf{Type}}
-   \newcommand{\unfold}{\textsf{unfold}}
-   \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra  #3$}}
-   \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}}
-   \newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]}
-   \newcommand{\WFE}[1]{\WF{E}{#1}}
-   \newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)}
-   \newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}
-   \newcommand{\with}{\kw{with}}
-   \newcommand{\WS}[3]{#1[] \vdash #2 <: #3}
-   \newcommand{\WSE}[2]{\WS{E}{#1}{#2}}
-   \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4}
-   \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
-   \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}}
-   \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}}
-   \newcommand{\zeroone}[1]{[{#1}]}
-   \newcommand{\zeros}{\textsf{zeros}}
-   \]
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 1fc267488c..38fdf243fe 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1,6 +1,3 @@
-.. include:: ../preamble.rst
-.. include:: ../replaces.rst
-
 .. _ltac:
 
 The tactic language
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index b1e769c571..3c0577b8e4 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -1,4 +1,3 @@
-.. include:: ../replaces.rst
 .. _proofhandling:
 
 -------------------
@@ -442,7 +441,12 @@ The following example script illustrates all these features:
    You tried to apply a tactic but no goals were under focus.
    Using :n:`@bullet` is  mandatory here.
 
-.. exn:: No such goal. Try unfocusing with %{.
+.. FIXME: the :noindex: below works around a Sphinx issue.
+   (https://github.com/sphinx-doc/sphinx/issues/4979)
+   It should be removed once that issue is fixed.
+
+.. exn:: No such goal. Try unfocusing with %}.
+   :noindex:
 
    You just finished a goal focused by ``{``, you must unfocus it with ``}``.
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 8656e5eb3e..361b6e44a5 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _thessreflectprooflanguage:
 
 ------------------------------
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index fb121c82ec..b0b57d00a0 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -1,6 +1,3 @@
-.. include:: ../preamble.rst
-.. include:: ../replaces.rst
-
 .. _tactics:
 
 Tactics
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 584193b9c6..56df535d85 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1,6 +1,3 @@
-.. include:: ../preamble.rst
-.. include:: ../replaces.rst
-
 .. _vernacularcommands:
 
 Vernacular commands
diff --git a/doc/sphinx/replaces.rst b/doc/sphinx/refman-preamble.rst
index 28a04f90ce..c662028773 100644
--- a/doc/sphinx/replaces.rst
+++ b/doc/sphinx/refman-preamble.rst
@@ -1,4 +1,13 @@
-.. some handy replacements for common items
+.. This file is automatically prepended to all other files using the ``rst_prolog`` option.
+
+.. only:: html
+
+   .. This is included once per page in the HTML build, and a single time (in the
+      document's preamble) in the LaTeX one.
+
+   .. preamble:: /refman-preamble.sty
+
+.. Some handy replacements for common items
 
 .. role:: smallcaps
 
@@ -21,7 +30,7 @@
 .. |class_2| replace:: `class`\ :math:`_{2}`
 .. |Coq| replace:: :smallcaps:`Coq`
 .. |CoqIDE| replace:: :smallcaps:`CoqIDE`
-.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\small{\beta\delta\iota\zeta}}`
+.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\beta\delta\iota\zeta}`
 .. |Gallina| replace:: :smallcaps:`Gallina`
 .. |ident_0| replace:: `ident`\ :math:`_{0}`
 .. |ident_1,1| replace:: `ident`\ :math:`_{1,1}`
diff --git a/doc/sphinx/refman-preamble.sty b/doc/sphinx/refman-preamble.sty
new file mode 100644
index 0000000000..b4fc608e47
--- /dev/null
+++ b/doc/sphinx/refman-preamble.sty
@@ -0,0 +1,88 @@
+\newcommand{\alors}{\textsf{then}}
+\newcommand{\alter}{\textsf{alter}}
+\newcommand{\as}{\kw{as}}
+\newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)}
+\newcommand{\bool}{\textsf{bool}}
+\newcommand{\case}{\kw{case}}
+\newcommand{\conc}{\textsf{conc}}
+\newcommand{\cons}{\textsf{cons}}
+\newcommand{\consf}{\textsf{consf}}
+\newcommand{\conshl}{\textsf{cons\_hl}}
+\newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)}
+\newcommand{\emptyf}{\textsf{emptyf}}
+\newcommand{\End}{\kw{End}}
+\newcommand{\kwend}{\kw{end}}
+\newcommand{\EqSt}{\textsf{EqSt}}
+\newcommand{\even}{\textsf{even}}
+\newcommand{\evenO}{\textsf{even}_\textsf{O}}
+\newcommand{\evenS}{\textsf{even}_\textsf{S}}
+\newcommand{\false}{\textsf{false}}
+\newcommand{\filter}{\textsf{filter}}
+\newcommand{\Fix}{\kw{Fix}}
+\newcommand{\fix}{\kw{fix}}
+\newcommand{\for}{\textsf{for}}
+\newcommand{\forest}{\textsf{forest}}
+\newcommand{\from}{\textsf{from}}
+\newcommand{\Functor}{\kw{Functor}}
+\newcommand{\haslength}{\textsf{has\_length}}
+\newcommand{\hd}{\textsf{hd}}
+\newcommand{\ident}{\textsf{ident}}
+\newcommand{\In}{\kw{in}}
+\newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)}
+\newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)}
+\newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)}
+\newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}}
+\newcommand{\injective}{\kw{injective}}
+\newcommand{\kw}[1]{\textsf{#1}}
+\newcommand{\lb}{\lambda}
+\newcommand{\length}{\textsf{length}}
+\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3}
+\newcommand{\List}{\textsf{list}}
+\newcommand{\lra}{\longrightarrow}
+\newcommand{\Match}{\kw{match}}
+\newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})}
+\newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})}
+\newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})}
+\newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})}
+\newcommand{\mto}{.\;}
+\newcommand{\Nat}{\mathbb{N}}
+\newcommand{\nat}{\textsf{nat}}
+\newcommand{\Nil}{\textsf{nil}}
+\newcommand{\nilhl}{\textsf{nil\_hl}}
+\newcommand{\nO}{\textsf{O}}
+\newcommand{\node}{\textsf{node}}
+\newcommand{\nS}{\textsf{S}}
+\newcommand{\odd}{\textsf{odd}}
+\newcommand{\oddS}{\textsf{odd}_\textsf{S}}
+\newcommand{\ovl}[1]{\overline{#1}}
+\newcommand{\Pair}{\textsf{pair}}
+\newcommand{\Prod}{\textsf{prod}}
+\newcommand{\Prop}{\textsf{Prop}}
+\newcommand{\return}{\kw{return}}
+\newcommand{\Set}{\textsf{Set}}
+\newcommand{\si}{\textsf{if}}
+\newcommand{\sinon}{\textsf{else}}
+\newcommand{\Sort}{\cal S}
+\newcommand{\Str}{\textsf{Stream}}
+\newcommand{\Struct}{\kw{Struct}}
+\newcommand{\subst}[3]{#1\{#2/#3\}}
+\newcommand{\tl}{\textsf{tl}}
+\newcommand{\tree}{\textsf{tree}}
+\newcommand{\true}{\textsf{true}}
+\newcommand{\Type}{\textsf{Type}}
+\newcommand{\unfold}{\textsf{unfold}}
+\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra  #3$}}
+\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}}
+\newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]}
+\newcommand{\WFE}[1]{\WF{E}{#1}}
+\newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)}
+\newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}
+\newcommand{\with}{\kw{with}}
+\newcommand{\WS}[3]{#1[] \vdash #2 <: #3}
+\newcommand{\WSE}[2]{\WS{E}{#1}{#2}}
+\newcommand{\WT}[4]{#1[#2] \vdash #3 : #4}
+\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
+\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}}
+\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}}
+\newcommand{\zeroone}[1]{[{#1}]}
+\newcommand{\zeros}{\textsf{zeros}}
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 4c0e85bdd4..0236f19490 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _syntaxextensionsandinterpretationscopes:
 
 Syntax extensions and interpretation scopes
diff --git a/doc/sphinx/zebibliography.html.rst b/doc/sphinx/zebibliography.html.rst
new file mode 100644
index 0000000000..756edd5482
--- /dev/null
+++ b/doc/sphinx/zebibliography.html.rst
@@ -0,0 +1,17 @@
+.. There are multiple issues with sphinxcontrib-bibtex that we have to work around:
+   - The list of cited entries is computed right after encountering
+     `.. bibliography`, so the file containing that command has to come last
+     alphabetically:
+     https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#unresolved-citations-across-documents
+   - `.. bibliography::` puts the bibliography on its own page with its own
+     title in LaTeX, but includes it inline without a title in HTML:
+     https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#mismatch-between-output-of-html-and-latex-backends
+
+.. _bibliography:
+
+==============
+ Bibliography
+==============
+
+.. bibliography:: biblio.bib
+   :cited:
diff --git a/doc/sphinx/zebibliography.rst b/doc/sphinx/zebibliography.latex.rst
index 0000caa301..2c0396f1c9 100644
--- a/doc/sphinx/zebibliography.rst
+++ b/doc/sphinx/zebibliography.latex.rst
@@ -1,8 +1,6 @@
-.. _bibliography:
+.. See zebibliography.html.rst for details
 
-============
-Bibliography
-============
+.. _bibliography:
 
 .. bibliography:: biblio.bib
    :cited:
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 40554c3ca3..2bf9776751 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -34,7 +34,7 @@ from sphinx.util.logging import getLogger
 from sphinx.directives import ObjectDescription
 from sphinx.domains import Domain, ObjType, Index
 from sphinx.domains.std import token_xrefs
-from sphinx.ext.mathbase import MathDirective, displaymath
+from sphinx.ext import mathbase
 
 from . import coqdoc
 from .repl import ansicolors
@@ -58,6 +58,15 @@ def make_target(objtype, targetid):
     """Create a target to an object of type objtype and id targetid"""
     return "coq:{}.{}".format(objtype, targetid)
 
+def make_math_node(latex, docname, nowrap):
+    node = mathbase.displaymath()
+    node['latex'] = latex
+    node['label'] = None # Otherwise equations are numbered
+    node['nowrap'] = nowrap
+    node['docname'] = docname
+    node['number'] = None
+    return node
+
 class CoqObject(ObjectDescription):
     """A generic Coq object for Sphinx; all Coq objects are subclasses of this.
 
@@ -101,7 +110,9 @@ class CoqObject(ObjectDescription):
         # Explicit object naming
         'name': directives.unchanged,
         # Silence warnings produced by report_undocumented_coq_objects
-        'undocumented': directives.flag
+        'undocumented': directives.flag,
+        # noindex omits this object from its index
+        'noindex': directives.flag
     }
 
     def subdomain_data(self):
@@ -138,6 +149,13 @@ class CoqObject(ObjectDescription):
             msg = MSG.format(name, self.env.doc2path(objects[name][0]))
             self.state_machine.reporter.warning(msg, line=self.lineno)
 
+    def _warn_if_duplicate_name(self, objects, name):
+        """Check that two objects in the same domain don't have the same name."""
+        if name in objects:
+            MSG = 'Duplicate object: {}; other is at {}'
+            msg = MSG.format(name, self.env.doc2path(objects[name][0]))
+            self.state_machine.reporter.warning(msg, line=self.lineno)
+
     def _record_name(self, name, target_id):
         """Record a name, mapping it to target_id
 
@@ -165,13 +183,16 @@ class CoqObject(ObjectDescription):
         """Add `name` (pointing to `target`) to the main index."""
         assert isinstance(name, str)
         if not name.startswith("_"):
-            index_text = name
+            # remove trailing . , found in commands, but not ... (ellipsis)
+            trim = name.endswith(".") and not name.endswith("...")
+            index_text = name[:-1] if trim else name
             if self.index_suffix:
                 index_text += " " + self.index_suffix
             self.indexnode['entries'].append(('single', index_text, target, '', None))
 
     def add_target_and_index(self, name, _, signode):
-        """Attach a link target to `signode` and an index entry for `name`."""
+        """Attach a link target to `signode` and an index entry for `name`.
+        This is only called (from ``ObjectDescription.run``) if ``:noindex:`` isn't specified."""
         if name:
             target = self._add_target(signode, name)
             self._add_index_entry(name, target)
@@ -487,7 +508,7 @@ def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]):
 CoqCodeRole = coq_code_role
 
 class CoqtopDirective(Directive):
-    """A reST directive to describe interactions with Coqtop.
+    r"""A reST directive to describe interactions with Coqtop.
 
     Usage::
 
@@ -525,16 +546,17 @@ class CoqtopDirective(Directive):
     required_arguments = 0
     optional_arguments = 1
     final_argument_whitespace = True
+    option_spec = { 'name': directives.unchanged }
     directive_name = "coqtop"
 
     def run(self):
         # Uses a ‘container’ instead of a ‘literal_block’ to disable
         # Pygments-based post-processing (we could also set rawsource to '')
         content = '\n'.join(self.content)
-        options = self.arguments[0].split() if self.arguments else ['in']
-        if 'all' in options:
-            options.extend(['in', 'out'])
-        node = nodes.container(content, coqtop_options = list(set(options)),
+        args = self.arguments[0].split() if self.arguments else ['in']
+        if 'all' in args:
+            args.extend(['in', 'out'])
+        node = nodes.container(content, coqtop_options = list(set(args)),
                                classes=['coqtop', 'literal-block'])
         self.add_name(node)
         return [node]
@@ -559,6 +581,7 @@ class CoqdocDirective(Directive):
     required_arguments = 0
     optional_arguments = 0
     final_argument_whitespace = True
+    option_spec = { 'name': directives.unchanged }
     directive_name = "coqdoc"
 
     def run(self):
@@ -567,6 +590,7 @@ class CoqdocDirective(Directive):
         content = '\n'.join(self.content)
         node = nodes.inline(content, '', *highlight_using_coqdoc(content))
         wrapper = nodes.container(content, node, classes=['coqdoc', 'literal-block'])
+        self.add_name(wrapper)
         return [wrapper]
 
 class ExampleDirective(BaseAdmonition):
@@ -602,24 +626,39 @@ class ExampleDirective(BaseAdmonition):
         self.options['classes'] = ['admonition', 'note']
         return super().run()
 
-class PreambleDirective(MathDirective):
-    r"""A reST directive for hidden math.
+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.
 
-    Example::
-
-       .. preamble::
+    Usage::
 
-          \newcommand{\paren}[#1]{\left(#1\right)}
+       .. preamble:: preamble.tex
     """
-
+    has_content = False
+    required_arguments = 1
+    optional_arguments = 0
+    final_argument_whitespace = True
+    option_spec = {}
     directive_name = "preamble"
 
     def run(self):
-        self.options['nowrap'] = True
-        [node] = super().run()
+        document = self.state.document
+        env = document.settings.env
+
+        if not document.settings.file_insertion_enabled:
+            msg = 'File insertion disabled'
+            return [document.reporter.warning(msg, line=self.lineno)]
+
+        rel_fname, abs_fname = env.relfn2path(self.arguments[0])
+        env.note_dependency(rel_fname)
+
+        with open(abs_fname, encoding="utf-8") as ltx:
+            latex = ltx.read()
+
+        node = make_math_node(latex, env.docname, nowrap=True)
         node['classes'] = ["math-preamble"]
+        set_source_info(self, node)
         return [node]
 
 class InferenceDirective(Directive):
@@ -632,8 +671,8 @@ class InferenceDirective(Directive):
 
        .. inference:: name
 
-          newline-separated premisses
-          ------------------------
+          newline-separated premises
+          --------------------------
           conclusion
 
     Example::
@@ -652,15 +691,6 @@ class InferenceDirective(Directive):
     final_argument_whitespace = True
     directive_name = "inference"
 
-    def make_math_node(self, latex):
-        node = displaymath()
-        node['latex'] = latex
-        node['label'] = None # Otherwise equations are numbered
-        node['nowrap'] = False
-        node['docname'] = self.state.document.settings.env.docname
-        node['number'] = None
-        return node
-
     @staticmethod
     def prepare_latex_operand(op):
         # TODO: Could use a fancier inference class in LaTeX
@@ -680,7 +710,8 @@ class InferenceDirective(Directive):
         title = self.arguments[0]
         content = '\n'.join(self.content)
         latex = self.prepare_latex(content)
-        math_node = self.make_math_node(latex)
+        docname = self.state.document.settings.env.docname
+        math_node = make_math_node(latex, docname, nowrap=False)
 
         tid = nodes.make_id(title)
         target = nodes.target('', '', ids=['inference-' + tid])
@@ -827,23 +858,28 @@ class CoqtopBlocksTransform(Transform):
             kept_node['classes'] = [c for c in kept_node['classes']
                                     if c != 'coqtop-hidden']
 
-    def merge_consecutive_coqtop_blocks(self):
+    @staticmethod
+    def merge_consecutive_coqtop_blocks(app, doctree, _):
         """Merge consecutive divs wrapping lists of Coq sentences; keep ‘dl’s separate."""
-        for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block):
+        for node in doctree.traverse(CoqtopBlocksTransform.is_coqtop_block):
             if node.parent:
+                rawsources, names = [node.rawsource], set(node['names'])
                 for sibling in node.traverse(include_self=False, descend=False,
                                              siblings=True, ascend=False):
                     if CoqtopBlocksTransform.is_coqtop_block(sibling):
-                        self.merge_coqtop_classes(node, sibling)
+                        CoqtopBlocksTransform.merge_coqtop_classes(node, sibling)
+                        rawsources.append(sibling.rawsource)
+                        names.update(sibling['names'])
                         node.extend(sibling.children)
                         node.parent.remove(sibling)
                         sibling.parent = None
                     else:
                         break
+                node.rawsource = "\n\n".join(rawsources)
+                node['names'] = list(names)
 
     def apply(self):
         self.add_coqtop_output()
-        self.merge_consecutive_coqtop_blocks()
 
 class CoqSubdomainsIndex(Index):
     """Index subclass to provide subdomain-specific indices.
@@ -1059,7 +1095,6 @@ def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint:
     pygments if available.  This prevents the LaTeX builder from getting
     confused.
     """
-
     is_html = app.builder.tags.has("html")
     for node in doctree.traverse(is_coqtop_or_coqdoc_block):
         if is_html:
@@ -1096,6 +1131,7 @@ def setup(app):
 
     app.add_transform(CoqtopBlocksTransform)
     app.connect('doctree-resolved', simplify_source_code_blocks_for_latex)
+    app.connect('doctree-resolved', CoqtopBlocksTransform.merge_consecutive_coqtop_blocks)
 
     # Add extra styles
     app.add_stylesheet("fonts.css")
@@ -1108,4 +1144,11 @@ def setup(app):
     # Tell Sphinx about extra settings
     app.add_config_value("report_undocumented_coq_objects", None, 'env')
 
-    return {'version': '0.1', "parallel_read_safe": True}
+    # ``env_version`` is used by Sphinx to know when to invalidate
+    # coqdomain-specific bits in its caches.  It should be incremented when the
+    # contents of ``env.domaindata['coq']`` change.  See
+    # `https://github.com/sphinx-doc/sphinx/issues/4460`.
+    meta = { "version": "0.1",
+             "env_version": 1,
+             "parallel_read_safe": True }
+    return meta