diff options
Diffstat (limited to 'doc')
| -rwxr-xr-x | 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 53bbd258c9..3fe782d905 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -161,6 +161,7 @@ \newcommand{\form}{\textrm{\textsl{form}}} \newcommand{\entry}{\textrm{\textsl{entry}}} \newcommand{\proditem}{\textrm{\textsl{production\_item}}} +\newcommand{\taclevel}{\textrm{\textsl{tactic\_level}}} \newcommand{\tacargtype}{\textrm{\textsl{tactic\_argument\_type}}} \newcommand{\scope}{\textrm{\textsl{scope}}} \newcommand{\optscope}{\textrm{\textsl{opt\_scope}}} |