diff options
| author | ppedrot | 2012-01-23 16:16:56 +0000 |
|---|---|---|
| committer | ppedrot | 2012-01-23 16:16:56 +0000 |
| commit | a9521af9d808e345917dd06445362427665a5846 (patch) | |
| tree | 3daf09b8494d10887d1c2fde09d38e728f3004df /plugins | |
| parent | e9de7c8232bc696e26114a35b674d221287ea248 (diff) | |
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
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/subtac/g_subtac.ml4 | 22 |
1 files changed, 20 insertions, 2 deletions
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: |