From 15f7e93adeb4342f6c255bdb2cf624a98b28034a Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 20 Jan 2012 18:57:06 +0000
Subject: This is a quick hack to permit the parsing of the locality flag in
 the Program subtactic. Ideally, locality flags should be handled in a nicer
 way...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14924 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/subtac/g_subtac.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index 89fbd6ffa4..de994d915b 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -52,8 +52,8 @@ GEXTEND Gram
   GLOBAL: subtac_gallina_loc typeclass_constraint subtac_withtac;
 
   subtac_gallina_loc:
-    [ [ g = Vernac.gallina -> loc, g
-    | g = Vernac.gallina_ext -> loc, g ] ]
+    [ [ Vernac.locality; g = Vernac.gallina -> loc, g
+    | Vernac.locality; g = Vernac.gallina_ext -> loc, g ] ]
     ;
 
   subtac_withtac:
-- 
cgit v1.2.3