From a9521af9d808e345917dd06445362427665a5846 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 23 Jan 2012 16:16:56 +0000
Subject: Another quick hack that works this time, to handle printing of
 locality in Program subtac.

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

(limited to 'plugins')

diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index 89fbd6ffa4..6aee94bae3 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -48,12 +48,30 @@ open Prim
 open Constr
 let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
 
+let enforce_locality arg =
+  let flag = !Vernacexpr.locality_flag in
+  match flag with
+  | None -> (* no locality flag set for now *)
+    Vernacexpr.locality_flag := arg
+  | Some _ -> (* a locality flag has been set, we cannot redefine it *)
+    begin match arg with
+    | None -> ()
+    | Some _ -> error "A locality flag has already been set."
+    end
+
 GEXTEND Gram
   GLOBAL: subtac_gallina_loc typeclass_constraint subtac_withtac;
 
+  (* FIXME : Program should be handled at a higher level in rule hierarchy. *)
+  subtac_locality:
+    [ [ IDENT "Local" -> enforce_locality (Some (loc, true))
+      | IDENT "Global" -> enforce_locality (Some (loc, false))
+      | -> enforce_locality None ] ]
+  ;
+
   subtac_gallina_loc:
-    [ [ g = Vernac.gallina -> loc, g
-    | g = Vernac.gallina_ext -> loc, g ] ]
+    [ [ subtac_locality; g = Vernac.gallina -> loc, g
+    | subtac_locality; g = Vernac.gallina_ext -> loc, g ] ]
     ;
 
   subtac_withtac:
-- 
cgit v1.2.3