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

46 files changed, 569 insertions, 251 deletions

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: