From 03d2931aad83cb7ce7383ee87fa80c108ac33dac Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Fri, 25 Jan 2019 01:55:05 +0900
Subject: Move \def\plus and \def\tri to refman-preamble.sty.

The definition of \plus and \tri in cic.rst is not effective
for HTML output.

So, move them into refman-preamble.sty.

Also, \tri is renamed to \trii to express
the suffix of "\triangleright_\iota".
---
 doc/sphinx/refman-preamble.sty | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'doc/sphinx/refman-preamble.sty')

diff --git a/doc/sphinx/refman-preamble.sty b/doc/sphinx/refman-preamble.sty
index b4fc608e47..cb7c8d0cf5 100644
--- a/doc/sphinx/refman-preamble.sty
+++ b/doc/sphinx/refman-preamble.sty
@@ -56,6 +56,7 @@
 \newcommand{\oddS}{\textsf{odd}_\textsf{S}}
 \newcommand{\ovl}[1]{\overline{#1}}
 \newcommand{\Pair}{\textsf{pair}}
+\newcommand{\plus}{\mathsf{plus}}
 \newcommand{\Prod}{\textsf{prod}}
 \newcommand{\Prop}{\textsf{Prop}}
 \newcommand{\return}{\kw{return}}
@@ -68,6 +69,7 @@
 \newcommand{\subst}[3]{#1\{#2/#3\}}
 \newcommand{\tl}{\textsf{tl}}
 \newcommand{\tree}{\textsf{tree}}
+\newcommand{\trii}{\triangleright_\iota}
 \newcommand{\true}{\textsf{true}}
 \newcommand{\Type}{\textsf{Type}}
 \newcommand{\unfold}{\textsf{unfold}}
-- 
cgit v1.2.3