and parg indent =
let module Con = Content in
function
- Con.Aux n -> prerr_endline ((blanks (indent+1)) ^ n);flush stderr
- | Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise");flush stderr
+ Con.Aux n -> prerr_endline ((blanks (indent+1)) ^ n)
+ | Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise")
+ | Con.Lemma lemma -> prerr_endline ((blanks (indent+1)) ^ "Lemma")
| Con.Term t ->
- prerr_endline ((blanks (indent+1)) ^ (CicPp.ppterm (Deannotate.deannotate_term t)));
- flush stderr
+ prerr_endline ((blanks (indent+1)) ^ (CicPp.ppterm (Deannotate.deannotate_term t)))
| Con.ArgProof p -> pproof p (indent+1)
- | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!");flush stderr
+ | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!")
;;
-let print_proof p = pproof p 0;
+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
+;;
+