- pat = OPT [
- "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] ->
- pat
- ];
- terms = LIST0 term SEP SYMBOL "," ->
- (match (pat, terms) with
- | None, [] -> TacticAst.Reduce (loc, kind, None)
- | None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal))
- | Some pat, [] -> fail loc "Missing term [list]"
- | Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat)))
+ p = OPT [ pattern_spec ] ->
+ let p = match p with None -> [], None | Some p -> p in
+ TacticAst.Reduce (loc, kind, p)
+ | 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)