Few modif in eta-fixing.

[helm.git] / helm / ocaml / cic_omdoc / contentPp.ml

diff --git a/helm/ocaml/cic_omdoc/contentPp.ml b/helm/ocaml/cic_omdoc/contentPp.ml
index 58ba4873b627bbed8d3bd7aef47ff0a2e815c500..3967c621668818fbb68b8e48fcd3e2bbc96e0b32 100644 (file)
--- 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 
+;;
+