diff options
| author | herbelin | 2004-03-03 14:36:11 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-03 14:36:11 +0000 |
| commit | ad8585656fe4c3e902aab93a4c470079640844a2 (patch) | |
| tree | 8b3c310f4e46e49a76b456fbf460548f77b346a9 /parsing | |
| parent | a4b41cdc8ab3c992b61ad85d68074bbdf44f4445 (diff) | |
Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5426 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egrammar.ml | 14 | ||||
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 10 |
2 files changed, 14 insertions, 10 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 8e3820c3a5..27f52e73a1 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 fd4647a620..70235d9ecf 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 |