| Replace (_, pattern, t) ->
sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t)
| Rewrite (_, pos, t, pattern, names) ->
sprintf "rewrite %s %s %s%s"
(if pos = `LeftToRight then ">" else "<")
| Replace (_, pattern, t) ->
sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t)
| Rewrite (_, pos, t, pattern, names) ->
sprintf "rewrite %s %s %s%s"
(if pos = `LeftToRight then ">" else "<")