%token OPTINCLUDE
%token RIGHT_ARRAY
%token RIGHT_PAREN
+%token SEMICOLON
%token <Ast.substs> STRING
%token <string> TACTIC
%token TACTIC_KEYWORD
stmts:
| (* none *) { Ast.Env.empty }
- | stmts INCLUDE STRING
+ | stmts INCLUDE STRING option(SEMICOLON)
{ do_include $1 $loc $3 false file }
- | stmts OPTINCLUDE STRING
+ | stmts OPTINCLUDE STRING option(SEMICOLON)
{ do_include $1 $loc $3 true file }
- | stmts stmt { let name, expr = $2 in Ast.Env.add name expr $1 }
+ | stmts stmt option(SEMICOLON)
+ { let name, expr = $2 in Ast.Env.add name expr $1 }
;
stmt:
expr:
| ID params { Ast.ECallGoal ($loc, $1, $2) }
| ID { Ast.EVar ($loc, $1) }
- | TACTIC params { Ast.ECallTactic ($loc, $1, $2) }
+ | TACTIC params { Ast.ETacticCtor ($loc, $1, $2) }
| STRING { Ast.ESubsts ($loc, $1) }
| LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) }
;