Cic2content split into Content and Cic2content.

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

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index c2d10e5199818b524612a44064e41496269dc01e..46585f14cd80c1036782f580c649f10ac5939de7 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -42,7 +42,7 @@ let rec split n l =
 
 let is_big_general countterm p =
   let maxsize = Cexpr2pres.maxsize in
-  let module Con = Cic2content in
+  let module Con = Content in
   let rec countp current_size p =
     if current_size > maxsize then current_size
     else 
@@ -143,7 +143,7 @@ let make_concl verb concl =
 ;;
 
 let make_args_for_apply term2pres args =
- let module Con = Cic2content in
+ let module Con = Content in
  let module P = Mpresentation in
  let rec make_arg_for_apply is_first arg row = 
    (match arg with 
@@ -168,7 +168,7 @@ let make_args_for_apply term2pres args =
  | _ -> assert false;;
 
 let rec justification term2pres p = 
-  let module Con = Cic2content in
+  let module Con = Content in
   let module P = Mpresentation in
   if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or
      ((p.Con.proof_context = []) &
@@ -183,7 +183,7 @@ let rec justification term2pres p =
      
 and proof2pres term2pres p =
   let rec proof2pres p =
-    let module Con = Cic2content in
+    let module Con = Content in
     let module P = Mpresentation in
       let indent = 
         let is_decl e = 
@@ -239,7 +239,7 @@ and proof2pres term2pres p =
 
   and ce2pres =
     let module P = Mpresentation in
-    let module Con = Cic2content in
+    let module Con = Content in
       function
         `Declaration d -> 
           (match d.Con.dec_name with
@@ -322,7 +322,7 @@ and proof2pres term2pres p =
         [P.Mtd ([], conclude_aux conclude)])
 
   and conclude_aux conclude =
-    let module Con = Cic2content in
+    let module Con = Content in
     let module P = Mpresentation in
     if conclude.Con.conclude_method = "TD_Conversion" then
       let expected = 
@@ -446,7 +446,7 @@ and proof2pres term2pres p =
 
   and arg2pres =
     let module P = Mpresentation in
-    let module Con = Cic2content in
+    let module Con = Content in
     function
         Con.Aux n -> 
           P.Mtext ([],"aux " ^ string_of_int n)
@@ -461,7 +461,7 @@ and proof2pres term2pres p =
  
    and byinduction conclude =
      let module P = Mpresentation in
-     let module Con = Cic2content in
+     let module Con = Content in
      let proof_conclusion = 
        (match conclude.Con.conclude_conclusion with
           None -> P.Mtext([],"No conclusion???")
@@ -507,7 +507,7 @@ and proof2pres term2pres p =
 
     and make_case =  
       let module P = Mpresentation in
-      let module Con = Cic2content in
+      let module Con = Content in
       function 
         Con.ArgProof p ->
           let name =
@@ -591,7 +591,7 @@ proof2pres p
 exception ToDo;;
 
 let content2pres term2pres (id,params,metasenv,obj) =
- let module Con = Cic2content in
+ let module Con = Content in
  let module P = Mpresentation in
   match obj with
      `Def (Con.Const,thesis,`Proof p) ->