diff options
| author | Clément Pit-Claudel | 2020-03-26 16:39:36 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-03-26 16:39:36 -0400 |
| commit | 5f5f9520ccf0f107d381e5874a3743f47e37c409 (patch) | |
| tree | 2c6d2567c74a853cae8cf9f76f82f08140cc32e7 | |
| parent | 3a34d96a9a8b570ca0c1e186d7c99683b3841e69 (diff) | |
| parent | 84ec585de78a961fe7a157cd9f34cd67be6af3ed (diff) | |
Merge PR #11929: Reintroduce a command that was actually used in another one. Fix build of PDF manual.
Reviewed-by: cpitclaudel
| -rw-r--r-- | doc/sphinx/refman-preamble.sty | 2 |
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}]} |