diff options
| -rw-r--r-- | parsing/g_corevernac.ml4 | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/parsing/g_corevernac.ml4 b/parsing/g_corevernac.ml4 index c6564d47c6..b8f5b30394 100644 --- a/parsing/g_corevernac.ml4 +++ b/parsing/g_corevernac.ml4 @@ -51,7 +51,7 @@ GEXTEND Gram (* Syntax entries for Grammar. Only grammar_entry is exported *) Prim.grammar_entry: [[ nont = Prim.ident; etyp = Prim.entry_type; ":="; - ep = entry_prec; rl = LIST0 grammar_rule SEP "|" -> + ep = entry_prec; OPT "|"; rl = LIST0 grammar_rule SEP "|" -> <:ast< (GRAMMARENTRY $nont $etyp $ep ($LIST rl)) >> ]] ; entry_prec: @@ -83,7 +83,8 @@ GEXTEND Gram (* Syntax entries for Syntax. Only syntax_entry is exported *) Prim.syntax_entry: - [ [ IDENT "level"; p = precedence; ":"; rl = LIST1 syntax_rule SEP "|" -> + [ [ IDENT "level"; p = precedence; ":"; + OPT "|"; rl = LIST1 syntax_rule SEP "|" -> <:ast< (SYNTAXENTRY $p ($LIST $rl)) >> ] ] ; syntax_rule: |