From 033d8f9628c54218378ee539648b6df6bfcbdb1e Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 20 Jan 2012 20:13:51 +0000
Subject: Reverted previous commit, which broke library compilation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14925 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 de994d915b..89fbd6ffa4 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:
-    [ [ Vernac.locality; g = Vernac.gallina -> loc, g
-    | Vernac.locality; g = Vernac.gallina_ext -> loc, g ] ]
+    [ [ g = Vernac.gallina -> loc, g
+    | g = Vernac.gallina_ext -> loc, g ] ]
     ;
 
   subtac_withtac:
-- 
cgit v1.2.3