diff options
Diffstat (limited to 'doc/common/macros.tex')
| -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 b21e0e9e2..2704a28af 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -140,6 +140,7 @@ \newcommand{\idparams}{\nterm{ident\_with\_params}} \newcommand{\statkwd}{\nterm{assertion\_keyword}} % vernac \newcommand{\termarg}{\nterm{arg}} +\newcommand{\hintdef}{\nterm{hint\_definition}} \newcommand{\typecstr}{\zeroone{{\tt :}~{\term}}} \newcommand{\typecstrwithoutblank}{\zeroone{{\tt :}{\term}}} |