- | 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;
+ id = OPT [ "as" ; id = IDENT -> id ];
+ p = OPT [ pattern_spec ] ->
+ let p = match p with None -> [], None | Some p -> p in
+ TacticAst.Generalize (loc,t,id,p)
+ | IDENT "goal"; n = NUM ->
+ TacticAst.Goal (loc, int_of_string n)
+ | IDENT "id" -> TacticAst.IdTac loc
+ | IDENT "injection"; t = term ->