| 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)))
| 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)))