+ | kind = reduction_kind;
+ pat = OPT [
+ "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] ->
+ pat
+ ];
+ terms = LIST0 term SEP SYMBOL "," ->
+ let tac =
+ (match (pat, terms) with
+ | None, [] -> TacticAst.Reduce (kind, None)
+ | None, terms -> TacticAst.Reduce (kind, Some (terms, `Goal))
+ | Some pat, [] -> TacticAst.Reduce (kind, Some ([], pat))
+ | Some pat, terms -> TacticAst.Reduce (kind, Some (terms, pat)))
+ in
+ return_tactic loc tac