| None ->
sprintf "_goal@%d" $startpos.pos_lnum, []
| Some x -> x in
- name, Ast.EGoal ($loc, (params, $2, $4, $5))
+ name, Ast.EGoalDefn ($loc, (params, $2, $4, $5))
}
| goal_stmt CODE
{
let name, params = $1 in
- name, Ast.EGoal ($loc, (params, [], [], Some $2))
+ name, Ast.EGoalDefn ($loc, (params, [], [], Some $2))
}
| TACTIC_KEYWORD TACTIC params_decl EQUALS CODE
{
- $2, Ast.ETactic ($loc, ($3, $5))
+ $2, Ast.ETacticDefn ($loc, ($3, $5))
}
| LET ID EQUALS expr { $2, $4 }
;
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) }
;