diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 |
3 files changed, 4 insertions, 1 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 *) |