aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/egrammar.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/egrammar.ml')
-rw-r--r--parsing/egrammar.ml14
1 files changed, 12 insertions, 2 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 8e3820c3a..27f52e73a 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -361,13 +361,23 @@ let rec interp_entry_name u s =
let t, g = interp_entry_name u (String.sub s 0 (l-4)) in
OptArgType t, Gramext.Sopt g
else
- let e = get_entry (get_univ u) s in
+ let e =
+ if !Options.v7 then get_entry (get_univ u) s
+ else
+ (* Qualified entries are no longer in use *)
+ try get_entry (get_univ "tactic") s
+ with _ ->
+ try get_entry (get_univ "prim") s
+ with _ ->
+ try get_entry (get_univ "constr") s
+ with _ -> error ("Unknown entry "^s)
+ in
let o = object_of_typed_entry e in
let t = type_of_typed_entry e in
t,Gramext.Snterm (Pcoq.Gram.Entry.obj o)
let qualified_nterm current_univ = function
- | NtQual (univ, en) -> (univ, en)
+ | NtQual (univ, en) -> if !Options.v7 then (univ, en) else assert false
| NtShort en -> (current_univ, en)
let make_vprod_item univ = function