diff options
Diffstat (limited to 'doc/common')
| -rwxr-xr-x | doc/common/macros.tex | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 1c4fa7e1f9..b464a96220 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -127,7 +127,9 @@ \newcommand{\ifitem}{\nterm{dep\_ret\_type}} \newcommand{\convclause}{\nterm{conversion\_clause}} \newcommand{\occclause}{\nterm{occurrence\_clause}} -\newcommand{\occset}{\nterm{occurrence\_set}} +\newcommand{\occgoalset}{\nterm{goal\_occurrences}} +\newcommand{\atoccurrences}{\nterm{at\_occurrences}} +\newcommand{\occlist}{\nterm{occurrences}} \newcommand{\params}{\nterm{params}} % vernac \newcommand{\returntype}{\nterm{return\_type}} \newcommand{\idparams}{\nterm{ident\_with\_params}} |