1 files changed, 4 insertions, 1 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 393b8547..2465d70f 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}}} 
@@ -182,6 +183,7 @@
 \newcommand{\name}{\textrm{\textsl{name}}}
 \newcommand{\num}{\textrm{\textsl{num}}}
 \newcommand{\pattern}{\textrm{\textsl{pattern}}}
+\newcommand{\orpattern}{\textrm{\textsl{or\_pattern}}}
 \newcommand{\intropattern}{\textrm{\textsl{intro\_pattern}}}
 \newcommand{\pat}{\textrm{\textsl{pat}}}
 \newcommand{\pgs}{\textrm{\textsl{pgms}}}
@@ -200,6 +202,7 @@
 \newcommand{\str}{\textrm{\textsl{string}}}
 \newcommand{\subsequentletter}{\textrm{\textsl{subsequent\_letter}}}
 \newcommand{\switch}{\textrm{\textsl{switch}}}
+\newcommand{\messagetoken}{\textrm{\textsl{message\_token}}}
 \newcommand{\tac}{\textrm{\textsl{tactic}}}
 \newcommand{\terms}{\textrm{\textsl{terms}}}
 \newcommand{\term}{\textrm{\textsl{term}}}
@@ -488,7 +491,7 @@
         {\begin{center}\begin{rulebox}}
         {\end{rulebox}\end{center}}
 
-% $Id: macros.tex 8606 2006-02-23 13:58:10Z herbelin $ 
+% $Id: macros.tex 9038 2006-07-11 13:53:53Z herbelin $ 
 
 
 %%% Local Variables: