diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 8 |
1 files changed, 6 insertions, 2 deletions
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" |