- | RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some (None,term) -> "conclude " ^ term_pp term | Some (Some name,term) -> "obtain (" ^ name ^ ") " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with `Auto params -> "_" ^ String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | `Term term2 -> term_pp term2) ^ (if cont then " done" else "")
+ | RewritingStep (_, term, term1, term2, cont) ->
+ (match term with
+ | None -> " "
+ | Some (None,term) -> "conclude " ^ term_pp term
+ | Some (Some name,term) ->
+ "obtain (" ^ name ^ ") " ^ term_pp term)
+ ^ "=" ^
+ term_pp term1 ^
+ (match term2 with
+ | `Auto params -> pp_auto_params ~term_pp params
+ | `Term term2 -> " exact " ^ term_pp term2
+ | `Proof -> " proof"
+ | `SolveWith term -> " using " ^ term_pp term)
+ ^ (if cont then " done" else "")