X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcontent2cic.ml;h=815e0caaac8b65ba68f519a2181d238a95786c2a;hb=e23bc37c0a5e552395e499e7b8cee8d610b8e4f4;hp=49468eafbefad7e1ae9484f5f0e502f6fd308ee7;hpb=4d7349fb1ecfb173f64fad0a97884d1d8e738904;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index 49468eafb..815e0caaa 100644
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -39,9 +39,9 @@ let proof2cic term2cic p =
     let module C = Cic in 
     let module Con = Content in
       let rec extend_premise_env current_env = 
-	function
+        function
             [] -> current_env
-	  | p::atl ->
+          | p::atl ->
               extend_premise_env 
               ((p.Con.proof_id,(proof2cic current_env p))::current_env) atl in
       let new_premise_env = extend_premise_env premise_env p.Con.proof_apply_context in
@@ -79,8 +79,45 @@ let proof2cic term2cic p =
                 C.LetIn (C.Name s, proof2cic premise_env p, target)
             | None -> 
                 C.LetIn (C.Anonymous, proof2cic premise_env p, target)) 
-      | `Joint ho -> 
-            raise TO_DO 
+      | `Joint {Con.joint_kind = kind; Con.joint_defs = defs} -> 
+            (match target with
+               C.Rel n ->
+                 (match kind with 
+                    `Recursive l ->
+                      let funs = 
+                        List.map2 
+                          (fun n bo ->
+                             match bo with
+                               `Proof bo ->
+                                  (match 
+                                    bo.Con.proof_conclude.Con.conclude_conclusion,
+                                    bo.Con.proof_name
+                                   with
+                                      Some ty, Some name -> 
+                                       (name,n,term2cic ty,proof2cic premise_env bo)
+                                    | _,_ -> assert false)
+                             | _ -> assert false)
+                          l defs in 
+                      C.Fix (n, funs)
+                  | `CoRecursive ->
+                     let funs = 
+                        List.map 
+                          (function bo ->
+                             match bo with
+                              `Proof bo ->
+                                 (match 
+                                    bo.Con.proof_conclude.Con.conclude_conclusion,
+                                    bo.Con.proof_name 
+                                  with
+                                     Some ty, Some name ->
+                                      (name,term2cic ty,proof2cic premise_env bo)
+                                   | _,_ -> assert false)
+                             | _ -> assert false)
+                           defs in 
+                      C.CoFix (n, funs)
+                  | _ -> (* no inductive types in local contexts *)
+                       assert false)
+             | _ -> assert false)
 
   and conclude2cic premise_env conclude =
     let module C = Cic in 
@@ -100,6 +137,10 @@ let proof2cic term2cic p =
     else if conclude.Con.conclude_method = "Exact" then
       (match conclude.Con.conclude_args with
          [Con.Term t] -> term2cic t
+       | [Con.Premise prem] -> 
+           (match prem.Con.premise_n with
+              None -> assert false
+            | Some n -> C.Rel n)
        | _ -> prerr_endline "3"; assert false)
     else if conclude.Con.conclude_method = "Intros+LetTac" then
       (match conclude.Con.conclude_args with