diff options
Diffstat (limited to 'doc')
| -rwxr-xr-x | doc/common/macros.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 8 |
2 files changed, 7 insertions, 3 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex index d0512c8525..1bae526179 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -168,7 +168,7 @@ \newcommand{\flag}{\nterm{flag}} \newcommand{\form}{\nterm{form}} \newcommand{\entry}{\nterm{entry}} -\newcommand{\proditem}{\nterm{production\_item}} +\newcommand{\proditem}{\nterm{prod\_item}} \newcommand{\taclevel}{\nterm{tactic\_level}} \newcommand{\tacargtype}{\nterm{tactic\_argument\_type}} \newcommand{\scope}{\nterm{scope}} diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index d1e2256365..be10ac4bf4 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -1089,11 +1089,11 @@ syntax \noindent \begin{tabular}{lcl} -{\sentence} & ::= & \texttt{Tactic Notation} \zeroone{\taclevel} \nelist{\proditem}{} \\ +{\sentence} & ::= & \zeroone{\tt Local} \texttt{Tactic Notation} \zeroone{\taclevel} \sequence{\proditem}{} \\ & & \texttt{:= {\tac} .}\\ {\proditem} & ::= & {\str} $|$ {\tacargtype}{\tt ({\ident})} \\ {\taclevel} & ::= & {\tt (at level} {\naturalnumber}{\tt )} \\ -{\tacargtype} & ::= & +{\tacargtype}\!\! & ::= & %{\tt preident} $|$ {\tt ident} $|$ {\tt simple\_intropattern} $|$ @@ -1171,6 +1171,10 @@ places where a list of the underlying entry can be used: {\nterm{entry}} is either {\tt\small constr}, {\tt\small hyp}, {\tt\small integer} or {\tt\small int\_or\_var}. +Tactic notations do not survive the end of sections. They survive +modules unless the command {\tt Local Tactic Notation} is used instead +of {\tt Tactic Notation}. + %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" |