diff options
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 | ||||
| -rw-r--r-- | plugins/subtac/g_subtac.ml4 | 4 |
4 files changed, 6 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 814ff9a397..10bf3f35a2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -69,7 +69,7 @@ let default_command_entry = let no_hook _ _ = () GEXTEND Gram - GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command; + GLOBAL: vernac gallina_ext locality tactic_mode noedit_mode subprf subgoal_command; vernac: FIRST [ [ IDENT "Time"; v = vernac -> VernacTime v | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 075440f1c6..6340e767f4 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -419,6 +419,7 @@ module Vernac_ = let vernac = gec_vernac "Vernac.vernac" let vernac_eoi = eoi_entry vernac let rec_definition = gec_vernac "Vernac.rec_definition" + let locality = gec_vernac "locality" (* Main vernac entry *) let main_entry = Gram.entry_create "vernac" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index bba0e56022..6610779254 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -237,6 +237,8 @@ module Vernac_ : val vernac : vernac_expr Gram.entry val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry val vernac_eoi : vernac_expr Gram.entry + (* FIXME: hack to handle locality in Program *) + val locality : unit Gram.entry end (** The main entry: reads an optional vernac command *) 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: |