From 84ec585de78a961fe7a157cd9f34cd67be6af3ed Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 26 Mar 2020 19:48:32 +0100
Subject: Reintroduce commands that were actually used. Fix build of PDF
 manual.

---
 doc/sphinx/refman-preamble.sty | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'doc')

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}]}
-- 
cgit v1.2.3