diff options
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 5f8106f2d0..36d7c3a7cb 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -21,7 +21,10 @@ GEXTEND Gram | g = gallina_ext; "." -> g | c = command; "." -> c | c = syntax; "." -> c - | "["; l = vernac_list_tail -> <:ast< (VernacList ($LIST $l)) >> ] ] + | "["; l = vernac_list_tail -> <:ast< (VernacList ($LIST $l)) >> + + (* This is for "Grammar vernac" rules *) + | id = Prim.metaident -> id ] ] ; vernac: FIRST [ [ IDENT "Time"; v = vernac -> <:ast< (Time $v)>> ] ] @@ -44,9 +47,9 @@ GEXTEND Gram GLOBAL: gallina gallina_ext; theorem_body_line: - [ [ n = numarg; ":"; tac = tacarg -> + [ [ n = numarg; ":"; tac = tacarg; "." -> <:ast< (VERNACCALL {SOLVE} $n (TACTIC $tac)) >> - | tac = tacarg -> <:ast< (VERNACCALL {SOLVE} 1 (TACTIC $tac)) >> + | tac = tacarg; "." -> <:ast< (VERNACCALL {SOLVE} 1 (TACTIC $tac)) >> ] ] ; theorem_body_line_list: |