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

1 files changed, 1 insertions, 1 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 7f63428c8..0e97b2a7f 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -227,6 +227,6 @@ GEXTEND Gram
   Vernac_.command:
     [ [ IDENT "Ltac";
         l = LIST1 tacdef_body SEP "with" ->
-          VernacDeclareTacticDefinition (true, l) ] ]
+          VernacDeclareTacticDefinition (use_module_locality (), true, l) ] ]
   ;
   END