| 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)
| Reflexivity _ -> "reflexivity"
| Replace (_, t1, t2) ->
sprintf "replace %s with %s" (pp_term_ast t1) (pp_term_ast t2)