diff options
| -rwxr-xr-x | doc/macros.tex | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/macros.tex b/doc/macros.tex index 108d716357..53c44176fb 100755 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -139,6 +139,8 @@ \newcommand{\tac}{\textrm{\textsl{tactic}}} \newcommand{\terms}{\textrm{\textsl{terms}}} \newcommand{\term}{\textrm{\textsl{term}}} +\newcommand{\module}{\textrm{\textsl{module}}} +\newcommand{\qualid}{\textrm{\textsl{qualid}}} \newcommand{\typedidents}{\textrm{\textsl{typed\_idents}}} \newcommand{\type}{\textrm{\textsl{type}}} \newcommand{\vref}{\textrm{\textsl{ref}}} |