- | Code (_,code) -> sprintf "(** %s. **)" (pp_executable code)
-
-let pp_statement = function
- | Executable (_, ex) -> pp_executable ex
- | Comment (_, c) -> pp_comment c
-
-let pp_cic_command = function
- | Include (_,path) -> "include " ^ path
- | Qed _ -> "qed"
- | Drop _ -> "drop"
- | Coercion (_,term,_add_composites) ->
- sprintf "coercion %s" (CicPp.ppterm term)
- | Set _
- | Alias _
- | Default _
- | Render _
- | Dump _
- | Interpretation _
- | Metadata _
- | Notation _
- | Obj _ -> assert false (* not implemented *)