- | IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n)
- | [ IDENT "injection" ]; t = term ->
+ | IDENT "fwd"; t = term ->
+ TacticAst.FwdSimpl (loc, t)
+ | IDENT "generalize"; t = tactic_term; p = OPT [ pattern_spec ] ->
+ let p = match p with None -> [], None | Some p -> p in
+ TacticAst.Generalize (loc,t,p)
+ | IDENT "goal"; n = NUM ->
+ TacticAst.Goal (loc, int_of_string n)
+ | IDENT "injection"; t = term ->