- | Reduce (_, kind, None)
- | Reduce (_, kind, Some ([], `Goal)) -> pp_reduction_kind kind
- | Reduce (_, kind, Some ([], `Everywhere)) ->
- sprintf "%s in hyp" (pp_reduction_kind kind)
- | Reduce (_, kind, Some (terms, `Goal)) ->
- sprintf "%s %s" (pp_reduction_kind kind)
- (String.concat ", " (List.map pp_term_ast terms))
- | Reduce (_, kind, Some (terms, `Everywhere)) ->
- sprintf "%s in hyp %s" (pp_reduction_kind kind)
- (String.concat ", " (List.map pp_term_ast terms))
- | ReduceAt (_, kind, id, term) ->
- sprintf "%s %s at %s" (pp_reduction_kind kind) id
- (pp_term_ast term)
+ | Reduce (_, kind, pat) ->
+ sprintf "%s %s" (pp_reduction_kind kind) (pp_pattern pat)