From feb92894c6be249abadd3303cfca3b258d6f3ea8 Mon Sep 17 00:00:00 2001
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 29 Sep 2009 15:11:52 +0000
Subject: Add support for Local Declare ML Module

Instead of failing with some obscure error message *after* loading the
module, accept Local Declare ML Module with the usual semantics.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12366 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'parsing/g_vernac.ml4')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4cd798e3e..f66b4ed1e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -582,7 +582,7 @@ GEXTEND Gram
 	s = [ s = ne_string -> s | s = IDENT -> s ] ->
 	  VernacLoad (verbosely, s)
       | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string ->
-	  VernacDeclareMLModule l
+	  VernacDeclareMLModule (use_locality (), l)
 
       | IDENT "Dump"; IDENT "Universes"; fopt = OPT ne_string ->
 	  error "This command is deprecated, use Print Universes"
-- 
cgit v1.2.3