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 17ba99ed8193797919c52f6981b2935b837670e6..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,38 +53,38 @@ 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
-        Con.Declaration d -> 
+        `Declaration d -> 
           (match d.Con.dec_name with
               Some s ->
                 C.Lambda (C.Name s, term2cic d.Con.dec_type, target)
             | None -> 
                 C.Lambda (C.Anonymous, term2cic d.Con.dec_type, target))
-      | Con.Hypothesis h ->
+      | `Hypothesis h ->
           (match h.Con.dec_name with
               Some s ->
                 C.Lambda (C.Name s, term2cic h.Con.dec_type, target)
             | None -> 
                 C.Lambda (C.Anonymous, term2cic h.Con.dec_type, target))
-      | Con.Proof p -> 
+      | `Proof p -> 
           (match p.Con.proof_name with
               Some s ->
                 C.LetIn (C.Name s, proof2cic premise_env p, target)
             | None -> 
                 C.LetIn (C.Anonymous, proof2cic premise_env p, target)) 
-      | Con.Definition d -> 
+      | `Definition d -> 
            (match d.Con.def_name with
               Some s ->
                 C.LetIn (C.Name s, proof2cic premise_env p, target)
             | None -> 
                 C.LetIn (C.Anonymous, proof2cic premise_env p, target)) 
-      | Con.Joint ho -> 
+      | `Joint ho -> 
             raise TO_DO 
 
   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 ->