sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
| Clear (_,id) -> sprintf "clear %s" id
| ClearBody (_,id) -> sprintf "clearbody %s" id
- | Compare (_,term) -> "compare " ^ term_pp term
| Constructor (_,n) -> "constructor " ^ string_of_int n
| Contradiction _ -> "contradiction"
| Cut (_, ident, term) ->
"cut " ^ term_pp term ^
(match ident with None -> "" | Some id -> " as " ^ id)
- | DecideEquality _ -> "decide equality"
| Decompose (_, [], what, names) ->
sprintf "decompose %s%s" what (pp_intros_specs (None, names))
| Decompose (_, types, what, names) ->