- | Coercion (_,term,_add_composites) ->
- sprintf "coercion %s" (CicPp.ppterm term)
- | Set _
- | Alias _
- | Default _
- | Render _
- | Dump _
- | Interpretation _
- | Notation _
- | Obj _ -> assert false (* not implemented *)
+ | Coercion (_,term, do_composites) ->
+ pp_coercion_cic term do_composites
+ | Obj (_,obj) -> CicPp.ppobj obj
+ | Set _-> assert false (* not implemented *)
+ | Alias (_, alias) -> pp_alias alias
+ | Default (_,what,uris) ->
+ pp_default what uris
+ | Render _ -> assert false (* not implemented *)
+ | Dump _ -> assert false (* not implemented *)
+ | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
+ pp_interpretation dsc symbol arg_patterns cic_appl_pattern
+ | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
+ pp_notation dir_opt l1_pattern assoc prec l2_pattern