Cic2content split into Content and Cic2content.

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

diff --git a/helm/ocaml/cic_transformations/contentPp.ml b/helm/ocaml/cic_transformations/contentPp.ml
index e42c987901fc7b7fded07eaff3e9077c86971d70..3bc8bb306ae6cf0896e2d662ab9c516218856751 100644 (file)
--- a/helm/ocaml/cic_transformations/contentPp.ml
+++ b/helm/ocaml/cic_transformations/contentPp.ml
@@ -58,8 +58,8 @@ let rec blanks n =
   if n = 0 then ""
   else (" " ^ (blanks (n-1)));; 
 
-let rec pproof (p: Cic.annterm Cic2content.proof) indent =
-  let module Con = Cic2content in
+let rec pproof (p: Cic.annterm Content.proof) indent =
+  let module Con = Content in
   let new_indent =
     (match p.Con.proof_name with
        Some s -> 
@@ -77,7 +77,7 @@ and pcontext c indent =
   List.iter (pcontext_element indent) c
 
 and pcontext_element indent =
-  let module Con = Cic2content in
+  let module Con = Content in
   function
       `Declaration d -> 
         (match d.Con.dec_name with
@@ -117,7 +117,7 @@ and papply_context ac indent =
   List.iter(function p -> (pproof p indent)) ac
 
 and pconclude concl indent =
-  let module Con = Cic2content in
+  let module Con = Content in
   prerr_endline ((blanks indent) ^ "Apply method " ^ concl.Con.conclude_method ^ " to");flush stderr;
   pargs concl.Con.conclude_args indent;
   match concl.Con.conclude_conclusion with
@@ -128,7 +128,7 @@ and pargs args indent =
   List.iter (parg indent) args
 
 and parg indent =
-  let module Con = Cic2content in
+  let module Con = Content in
   function
        Con.Aux n ->  prerr_endline ((blanks (indent+1)) ^ (string_of_int n));flush stderr
     |  Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise");flush stderr