X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2FcontentPp.ml;h=3967c621668818fbb68b8e48fcd3e2bbc96e0b32;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=58ba4873b627bbed8d3bd7aef47ff0a2e815c500;hpb=414dc18cdbc1f431758cfce79b0b7827e2419d39;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/contentPp.ml b/helm/ocaml/cic_omdoc/contentPp.ml
index 58ba4873b..3967c6216 100644
--- a/helm/ocaml/cic_omdoc/contentPp.ml
+++ b/helm/ocaml/cic_omdoc/contentPp.ml
@@ -139,7 +139,17 @@ and parg indent =
     | 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 
+;;
+