| LocatedTactic (loc, tac) -> pp_tactic tac
| Absurd term -> "absurd" ^ pp_term term
| Apply term -> "apply " ^ pp_term term
+ | Auto -> "auto"
| Assumption -> "assumption"
| Change (t1, t2, where) ->
sprintf "change %s with %s%s" (pp_term t1) (pp_term t2)