[doc] Move the LaTeX preamble to a separate .tex file

3 files changed, 97 insertions, 97 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 983f4e665f..ab4648d577 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -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
 =========
diff --git a/doc/sphinx/preamble.rst b/doc/sphinx/preamble.rst
index 395f558a85..dcbc3322ac 100644
--- a/doc/sphinx/preamble.rst
+++ b/doc/sphinx/preamble.rst
@@ -1,92 +1,6 @@
-.. preamble::
+.. only:: html
 
-   \[
-   \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}}
-   \]
+   .. 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/preamble.tex b/doc/sphinx/preamble.tex
new file mode 100644
index 0000000000..b4fc608e47
--- /dev/null
+++ b/doc/sphinx/preamble.tex
@@ -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}}