let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
let pp_reduction_kind ~term_pp = function
- | `Demodulate -> "demodulate"
| `Normalize -> "normalize"
| `Reduce -> "reduce"
| `Simpl -> "simplify"
in
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
| Elim (_, term, using, num, idents) ->
sprintf "elim " ^ term_pp term ^