From ca341a63254abea7c4f20ee3c6af485d2362497c Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 2 Sep 2009 20:47:46 +0000
Subject: Postpone checking of Local/Global to allow grammar extensions to use
 it too.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12304 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4      | 3 +--
 toplevel/vernacentries.ml | 3 +++
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d10a2950ce..9940a13784 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -67,8 +67,7 @@ GEXTEND Gram
   vernac: FIRST
     [ [ IDENT "Time"; v = vernac -> VernacTime v 
       | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
-      | locality; v = vernac_aux -> 
-	  check_locality (); v ] ]
+      | locality; v = vernac_aux -> v ] ]
   ;
   vernac_aux:
     (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 0e11ba582a..739193f518 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1406,3 +1406,6 @@ let interp c = match c with
 
   (* Extensions *)
   | VernacExtend (opn,args) -> Vernacinterp.call (opn,args)
+
+let interp c = interp c ; check_locality ()
+
-- 
cgit v1.2.3