aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/common
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2015-11-03 13:28:57 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-10 09:35:13 +0100
commitfc73973844f848fafb61b6aa39a327e95f09c129 (patch)
tree869b2a707f5ab7ee8f8debc0130dff33f6a9558c /doc/common
parent27c19fffda5c5b1f119a1b2115915b330fdfe1ba (diff)
CLEANUP: s/List_A/List~A/g
Diffstat (limited to 'doc/common')
-rw-r--r--doc/common/macros.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index a6240ad28..2271a8f13 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -261,7 +261,7 @@
\newcommand{\length}{\mbox{\textsf{length}}}
\newcommand{\haslengthA}{\mbox {\textsf{has\_length~A}}}
\newcommand{\List}{\mbox{\textsf{list}}}
-\newcommand{\ListA}{\mbox{\textsf{List\_A}}}
+\newcommand{\ListA}{\mbox{\textsf{List}~A}}
\newcommand{\nilhl}{\mbox{\textsf{nil\_hl}}}
\newcommand{\conshl}{\mbox{\textsf{cons\_hl}}}
\newcommand{\nat}{\mbox{\textsf{nat}}}