aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/common
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2015-11-02 14:41:37 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-10 09:35:11 +0100
commit47377fa44143d409331dd7d0c662e6ebb34d9f4f (patch)
tree9156837d378eec6891603842f7da3efe1971d32c /doc/common
parentc5b3e7ff66e1675aaec7be5e0ee6772e88250991 (diff)
ENH: The beginning of Section 4.5 (Inductive declarations) was changed in order to make it more concrete and more comprehensible.
This ver
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 ff13ec455..fb9190a16 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -260,7 +260,7 @@
\newcommand{\Length}{\mbox{\textsf{Length}}}
\newcommand{\length}{\mbox{\textsf{length}}}
\newcommand{\LengthA}{\mbox {\textsf{Length\_A}}}
-\newcommand{\List}{\mbox{\textsf{List}}}
+\newcommand{\List}{\mbox{\textsf{list}}}
\newcommand{\ListA}{\mbox{\textsf{List\_A}}}
\newcommand{\LNil}{\mbox{\textsf{Lnil}}}
\newcommand{\LCons}{\mbox{\textsf{Lcons}}}