diff options
Diffstat (limited to 'doc/common')
| -rw-r--r-- | doc/common/macros.tex | 1 |
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}} |