diff options
| author | herbelin | 2000-01-11 09:34:10 +0000 |
|---|---|---|
| committer | herbelin | 2000-01-11 09:34:10 +0000 |
| commit | df75cf61c8fb77a0b0097c761d42cf6057f11805 (patch) | |
| tree | 4a7f172f3d3a7f6388b2fa52e7cf59b59e5f0ecd | |
| parent | 5ccef151ea7fb56a3b3b10f74fa6c6f0577ea017 (diff) | |
Ajout '|' en tete de filtrage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@273 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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: |