-let pp_cic_command = function
- | Include (_,path) -> "include " ^ path
- | Qed _ -> "qed"
- | Drop _ -> "drop"
- | 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
-