diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 8 | ||||
| -rw-r--r-- | parsing/g_prim.ml4 | 3 |
2 files changed, 6 insertions, 5 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 1dfc5790f5..9fa0323986 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -192,19 +192,19 @@ END; GEXTEND Gram GLOBAL: syntax Prim.syntax_entry Prim.grammar_entry; - grammar_univ: + univ: [ [ univ = IDENT -> let _ = set_default_action_parser_by_name univ in univ ] ] ; syntax: [ [ "Token"; s = STRING; "." -> <:ast< (TOKEN ($STR $s)) >> - | "Grammar"; univ = grammar_univ; + | "Grammar"; univ = univ; tl = LIST1 Prim.grammar_entry SEP "with"; "." -> <:ast< (GRAMMAR ($VAR univ) (ASTLIST ($LIST tl))) >> - | "Syntax"; whatfor=IDENT; el=LIST1 Prim.syntax_entry SEP ";"; "." -> - <:ast< (SYNTAX ($VAR whatfor) (ASTLIST ($LIST el))) >> + | "Syntax"; univ = univ; el=LIST1 Prim.syntax_entry SEP ";"; "." -> + <:ast< (SYNTAX ($VAR univ) (ASTLIST ($LIST el))) >> | IDENT "Infix"; as_ = entry_prec; n = numarg; op = Prim.string; p = identarg; "." -> <:ast< (INFIX (AST $as_) $n $op $p) >> | IDENT "Distfix"; as_ = entry_prec; n = numarg; s = Prim.string; diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 239277828f..35d329177c 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -46,7 +46,8 @@ GEXTEND Gram (* meta-syntax entries *) astpat: - [ [ a = ast -> Node loc "ASTPAT" [a] ] ] + [ [ "<<" ; a = ast; ">>" -> Node loc "ASTPAT" [a] + | a = default_action_parser -> Node loc "ASTPAT" [a] ] ] ; astact: [ [ a = action -> Node loc "ASTACT" [a] ] ] |