- | Decompose (_, [], what, names) ->
- sprintf "decompose %s%s" (opt_string_pp what) (pp_intros_specs (None, names))
- | Decompose (_, types, what, names) ->
- let to_ident = function
- | Ident id -> id
- | Type _ -> assert false
- 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 ^
+ | Decompose (_, names) ->
+ Printf.sprintf "decompose%s"
+ (pp_intros_specs "names " (None, names))
+ | Demodulate (_, params) -> "demodulate " ^ pp_auto_params ~term_pp params
+ | Destruct (_, None) -> "destruct"
+ | Destruct (_, Some terms) -> "destruct " ^ pp_terms terms
+ | Elim (_, what, using, pattern, specs) ->
+ Printf.sprintf "elim %s%s %s%s"
+ (term_pp what)