- | kind = reduction_kind;
- 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)))
- | kind = reduction_kind; where = IDENT ; IDENT "at" ; pat = term ->
- TacticAst.ReduceAt (loc, kind, where, pat)
- | [ IDENT "reflexivity" ] ->
+ | kind = reduction_kind; p = OPT [ pattern_spec ] ->
+ let p = match p with None -> [], None | Some p -> p in
+ TacticAst.Reduce (loc, kind, p)
+ | IDENT "reflexivity" ->