- | Cut (_, term) -> "cut " ^ pp_term_ast term
- | Decompose (_, ident, principles) ->
- sprintf "decompose %s %s" (pp_idents principles) ident
- | Discriminate (_, ident) -> "discriminate " ^ ident
- | Elim (_, term, using) ->
+ | Cut (_, ident, term) ->
+ "cut " ^ pp_term_ast 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) ->
+ 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) what (pp_intros_specs (None, names))
+ | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term
+ | Elim (_, term, using, num, idents) ->