aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/common/macros.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/common/macros.tex')
-rw-r--r--doc/common/macros.tex1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 81def1674..6a28c5b3d 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -182,6 +182,7 @@
\newcommand{\declnotation}{\nterm{decl\_notation}}
\newcommand{\symbolentry}{\nterm{symbol}}
\newcommand{\modifiers}{\nterm{modifiers}}
+\newcommand{\binderinterp}{\nterm{binder\_interp}}
\newcommand{\localdef}{\nterm{local\_def}}
\newcommand{\localdecls}{\nterm{local\_decls}}
\newcommand{\ident}{\nterm{ident}}