[doc] Include the rst and LaTeX preambles automatically in all files

32 files changed, 18 insertions, 67 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index ab4648d577..fbf94fd7da 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -396,7 +396,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..4ca5171166 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -174,7 +174,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..5eba539e03 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
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 78471700be..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:
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/conf.py b/doc/sphinx/conf.py
index 35c08fd806..8b29d1e9f9 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -36,6 +36,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.
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index 797a9a9714..5bb7bf542c 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -1,6 +1,3 @@
-.. include:: preamble.rst
-.. include:: replaces.rst
-
 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
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 13d6e228a6..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:
 
 
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..ae96a75a94 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|
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/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 e8fc29dece..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
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 dcbc3322ac..0000000000
--- a/doc/sphinx/preamble.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-.. 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:: /preamble.tex
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..53294bf8da 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:
 
 -------------------
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..aa581e1ee1 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
 
diff --git a/doc/sphinx/preamble.tex b/doc/sphinx/refman-preamble.sty
index b4fc608e47..b4fc608e47 100644
--- a/doc/sphinx/preamble.tex
+++ b/doc/sphinx/refman-preamble.sty
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