diff options
| author | herbelin | 2012-08-11 17:45:12 +0000 |
|---|---|---|
| committer | herbelin | 2012-08-11 17:45:12 +0000 |
| commit | d71a32d3700980c07af2d7858147598b961607d6 (patch) | |
| tree | 1f4a02824f41c83d8260b655d1b601ad1775d4b3 /doc/refman | |
| parent | 7ac5be3b1e433c028b55c44f0ddfe805634ff0f1 (diff) | |
Added support for option Local (at module level) in Tactic Notation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15731 85f007b7-540e-0410-9357-904b9bb8a0f7
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" |