-(*
- | RewritingStep (_, term, term1, term2, cont) ->
- (match term with
- | None -> " "
- | Some (None,term) -> "conclude " ^ NotationPp.pp_term status term
- | Some (Some name,term) ->
- "obtain (" ^ name ^ ") " ^ NotationPp.pp_term status term)
- ^ "=" ^
- NotationPp.pp_term status term1 ^
- (match term2 with
- | `Auto params -> pp_auto_params params status
- | `Term term2 -> " exact " ^ NotationPp.pp_term status term2
- | `Proof -> " proof"
- | `SolveWith term -> " using " ^ NotationPp.pp_term status term)
- ^ (if cont then " done" else "")
-*)