diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-11 17:45:12 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-11 17:45:12 +0000 |
| commit | d71a32d3700980c07af2d7858147598b961607d6 (patch) | |
| tree | 1f4a02824f41c83d8260b655d1b601ad1775d4b3 /doc | |
| 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')
| -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 d0512c852..1bae52617 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 d1e225636..be10ac4bf 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" |