Cic2content split into Content and Cic2content.

[helm.git] / helm / gTopLevel / content2cic.ml

diff --git a/helm/gTopLevel/content2cic.ml b/helm/gTopLevel/content2cic.ml
index a4f8cd1ae4a0c99b04dd08662acd9c1529756797..e8a95fc892f7984afb25ede9f630279afe3fb859 100644 (file)
--- a/helm/gTopLevel/content2cic.ml
+++ b/helm/gTopLevel/content2cic.ml
@@ -37,7 +37,7 @@ exception TO_DO;;
 let proof2cic term2cic p =
   let rec proof2cic premise_env p =
     let module C = Cic in 
-    let module Con = Cic2content in
+    let module Con = Content in
       let rec extend_premise_env current_env = 
        function
             [] -> current_env
@@ -53,7 +53,7 @@ let proof2cic term2cic p =
 
   and ce2cic premise_env ce target =
     let module C = Cic in
-    let module Con = Cic2content in
+    let module Con = Content in
       match ce with
         `Declaration d -> 
           (match d.Con.dec_name with
@@ -84,7 +84,7 @@ let proof2cic term2cic p =
 
   and conclude2cic premise_env conclude =
     let module C = Cic in 
-    let module Con = Cic2content in
+    let module Con = Content in
     if conclude.Con.conclude_method = "TD_Conversion" then
       (match conclude.Con.conclude_args with
          [Con.ArgProof p] -> proof2cic [] p (* empty! *)
@@ -133,7 +133,7 @@ let proof2cic term2cic p =
 
   and arg2cic premise_env =
     let module C = Cic in
-    let module Con = Cic2content in
+    let module Con = Content in
     function
         Con.Aux n -> prerr_endline "8"; assert false
       | Con.Premise prem ->