From a29edb0a5e9d420a3780a7034aad4ef9cfe7c148 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 26 Oct 2009 14:46:43 +0000
Subject: 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
---
 parsing/g_ltac.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'parsing/g_ltac.ml4')

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