Reintroduce commands that were actually used. Fix build of PDF manual.

1 files changed, 2 insertions, 0 deletions

diff --git a/doc/sphinx/refman-preamble.sty b/doc/sphinx/refman-preamble.sty
index 718a54ba8f..629c30a793 100644
--- a/doc/sphinx/refman-preamble.sty
+++ b/doc/sphinx/refman-preamble.sty
@@ -20,6 +20,7 @@
 \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{\length}{\textsf{length}}
 \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3}
@@ -67,3 +68,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}]}