TacticAst.Fourier loc
| IDENT "fwd"; t = term ->
TacticAst.FwdSimpl (loc, t)
- | IDENT "generalize"; t = tactic_term; p = OPT [ pattern_spec ] ->
+ | 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,p)
+ TacticAst.Generalize (loc,t,id,p)
| IDENT "goal"; n = NUM ->
TacticAst.Goal (loc, int_of_string n)
| IDENT "injection"; t = term ->