New cleaning phase of the Local/Global option management

- Clarification and documentation of the different styles of
  Local/Global modifiers in vernacexpr.ml
- Addition of Global in sections for Open/Close Scope.
- Addition of Local for Ltac when not in sections.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12418 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 11 insertions, 1 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 3948bbe855..8be2e0b06c 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -186,7 +186,7 @@ is understood as
 \begin{figure}[ht]
 \begin{centerframe}
 \begin{tabular}{lcl}
-\nterm{top} & ::= & {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\
+\nterm{top} & ::= & \zeroone{\tt Local} {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\
 \\
 \nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=}
 {\tacexpr}\\
@@ -864,6 +864,9 @@ A previous definition of \qualid must exist in the environment.
 The new definition will always be used instead of the old one and
 it goes accross module boundaries.
 
+If preceded by the keyword {\tt Local} the tactic definition will not
+be exported outside the current module.
+
 \subsection[Printing {\ltac} tactics]{Printing {\ltac} tactics\comindex{Print Ltac}}
 
 Defined {\ltac} functions can be displayed using the command
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index a5678eacf4..d37fc9f3fc 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -700,6 +700,13 @@ exported to the modules that import the module where they occur.
 These variants are not exported to the modules that import the module
 where they occur, even if outside a section.
 
+\item {\tt Global Open Scope} {\scope}.
+
+\item {\tt Global Close Scope} {\scope}.
+
+These variants survive sections. They behave as if {\tt Global} were
+absent when not inside a section.
+
 \end{Variants}
 
 \subsection{Local interpretation rules for notations}