diff options
| -rw-r--r-- | parsing/egrammar.ml | 14 | ||||
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 10 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 5 |
3 files changed, 16 insertions, 13 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 diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index fd4647a62..70235d9ec 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -724,14 +724,8 @@ GEXTEND Gram ; production_item: [[ s = ne_string -> VTerm s - | nt = non_terminal; po = OPT [ "("; p = ident; ")" -> p ] -> - VNonTerm (loc,nt,po) ]] - ; - non_terminal: - [[ u = IDENT; ":"; nt = IDENT -> - NtQual(rename_command_entry u, rename_command_entry nt) - | IDENT "constr" -> NtQual ("constr","constr") - | nt = IDENT -> NtShort (rename_command_entry nt) ]] + | nt = IDENT; po = OPT [ "("; p = ident; ")" -> p ] -> + VNonTerm (loc,NtShort nt,po) ]] ; END diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 44599e72f..cfeb12f06 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -132,8 +132,7 @@ let pr_set_entry_type = function | ETBigint -> str "bigint" let pr_non_terminal = function - | NtQual ("constr","constr") -> str "constr" - | NtQual (u,nt) -> str u ++ str" : " ++ str nt + | NtQual (u,nt) -> (* no more qualified entries *) str nt | NtShort "constrarg" -> str "constr" | NtShort nt -> str nt @@ -416,7 +415,7 @@ let pr_grammar_tactic_rule (name,(s,pil),t) = *) hov 2 (str "Tactic Notation" ++ spc() ++ hov 0 (qsnew s ++ spc() ++ prlist_with_sep sep pr_production_item pil ++ - spc() ++ str":= " ++ spc() ++ pr_raw_tactic t)) + spc() ++ str":=" ++ spc() ++ pr_raw_tactic t)) let pr_box b = let pr_boxkind = function | PpHB n -> str"h" ++ spc() ++ int n |