diff options
Diffstat (limited to 'parsing/g_vernacnew.ml4')
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 10 |
1 files changed, 2 insertions, 8 deletions
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 |