| Reduce (_, kind, pat) ->
sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat)
| Reflexivity _ -> "reflexivity"
| Replace (_, pattern, t) ->
sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t)
| Reduce (_, kind, pat) ->
sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat)
| Reflexivity _ -> "reflexivity"
| Replace (_, pattern, t) ->
sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t)