diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-09 11:06:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-09 11:06:52 +0000 |
| commit | d72efb0925569f66506348f9886003e003bde7e8 (patch) | |
| tree | 8ff1d8b9809474d9e21b4978e7b0fbeab1b30f98 | |
| parent | 511df45b436bbc4811b84e901f76c48c5b477d36 (diff) | |
Bug point final dans la syntaxe theorem_body
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1365 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 5f8106f2d..36d7c3a7c 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: |