diff options
| -rwxr-xr-x | doc/macros.tex | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/macros.tex b/doc/macros.tex index 4c940d5226..6b3c2ed3b0 100755 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -87,6 +87,8 @@ \newcommand{\Index}{\textrm{\textsl{index}}} \newcommand{\abbrev}{\textrm{\textsl{abbreviation}}} \newcommand{\annotation}{\textrm{\textsl{annotation}}} +\newcommand{\returntype}{\textrm{\textsl{return\_type}}} +\newcommand{\caseitem}{\textrm{\textsl{case\_item}}} \newcommand{\atomictac}{\textrm{\textsl{atomic\_tactic}}} \newcommand{\binders}{\textrm{\textsl{bindings}}} \newcommand{\binder}{\textrm{\textsl{binding}}} @@ -126,6 +128,7 @@ \newcommand{\nestedpattern}{\textrm{\textsl{nested\_pattern}}} \newcommand{\num}{\textrm{\textsl{num}}} \newcommand{\params}{\textrm{\textsl{params}}} +\newcommand{\binderlet}{\textrm{\textsl{binder\_let}}} \newcommand{\pattern}{\textrm{\textsl{pattern}}} \newcommand{\pat}{\textrm{\textsl{pat}}} \newcommand{\pgs}{\textrm{\textsl{pgms}}} |