let types = List.rev_map to_ident types in
sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names))
| Demodulate _ -> "demodulate"
- | Discriminate (_, term) -> "discriminate " ^ term_pp term
+ | Destruct (_, term) -> "destruct " ^ term_pp term
| Elim (_, term, using, num, idents) ->
sprintf "elim " ^ term_pp term ^
(match using with None -> "" | Some term -> " using " ^ term_pp term)
| Fail _ -> "fail"
| Fourier _ -> "fourier"
| IdTac _ -> "id"
- | Injection (_, term) -> "injection " ^ term_pp term
| Intros (_, None, []) -> "intros"
| Inversion (_, term) -> "inversion " ^ term_pp term
| Intros (_, num, idents) ->