exception ContentPpInternalError;;
exception NotEnoughElements;;
+exception TO_DO
(* Utility functions *)
if n = 0 then ""
else (" " ^ (blanks (n-1)));;
-let rec pproof p indent =
+let rec pproof (p: Cic.annterm Cic2content.proof) indent =
let module Con = Cic2content in
let new_indent =
(match p.Con.proof_name with
and pcontext_element indent =
let module Con = Cic2content in
function
- Con.Declaration d ->
+ `Declaration d ->
(match d.Con.dec_name with
Some s ->
prerr_endline
flush stderr
| None ->
prerr_endline ((blanks indent) ^ "NO NAME!!"))
- | Con.Hypothesis h ->
+ | `Hypothesis h ->
(match h.Con.dec_name with
Some s ->
prerr_endline
flush stderr
| None ->
prerr_endline ((blanks indent) ^ "NO NAME!!"))
- | Con.Proof p -> pproof p indent
- | Con.Definition d ->
+ | `Proof p -> pproof p indent
+ | `Definition d ->
(match d.Con.def_name with
Some s ->
prerr_endline
flush stderr
| None ->
prerr_endline ((blanks indent) ^ "NO NAME!!"))
- | Con.Joint ho ->
+ | `Joint ho ->
prerr_endline ((blanks indent) ^ "Joint Def");
flush stderr
flush stderr
| Con.ArgProof p -> pproof p (indent+1)
| Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!");flush stderr
-
;;
let print_proof p = pproof p 0;
+
+