From d71a32d3700980c07af2d7858147598b961607d6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 11 Aug 2012 17:45:12 +0000
Subject: 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
---
 doc/common/macros.tex     | 2 +-
 doc/refman/RefMan-syn.tex | 8 ++++++--
 2 files changed, 7 insertions(+), 3 deletions(-)

(limited to 'doc')

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"
-- 
cgit v1.2.3