+let print_proof p = pproof p 0;;
+
+let print_obj (_,_,_,obj) =
+ match obj with
+ `Decl (_,decl) ->
+ pcontext_element 0 (decl:> Cic.annterm Content.in_proof_context_element)
+ | `Def (_,_,def) ->
+ pcontext_element 0 (def:> Cic.annterm Content.in_proof_context_element)
+ | `Joint _ as jo -> pcontext_element 0 jo
+;;
+