X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcontent2cic.ml;h=339492d1985317911dad12a0890d5a89d62fea25;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=d25d7942595f8b20348b1dc37596516f678f3dfd;hpb=c43f710f5e23e940114b1623329f650814e783af;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index d25d79425..339492d19 100644
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -149,10 +149,13 @@ let proof2cic deannotate p =
       (match conclude.Con.conclude_args with
          [Con.ArgProof p] -> proof2cic [] p (* empty! *)
        | _ -> prerr_endline "4"; assert false)
-    else if (conclude.Con.conclude_method = "ByInduction") then
+    else if (conclude.Con.conclude_method = "ByInduction" ||
+             conclude.Con.conclude_method = "AndInd" ||
+             conclude.Con.conclude_method = "Exists" ||
+             conclude.Con.conclude_method = "FalseInd") then
       (match (List.tl conclude.Con.conclude_args) with
-         Con.Term (C.AAppl 
-            id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args ->
+         Con.Term (C.AAppl (
+            id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))::args ->
            let subst =
              List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in 
            let cargs = args2cic premise_env args in
@@ -177,14 +180,14 @@ let proof2cic deannotate p =
              List.map 
                (function 
                    Con.ArgProof p -> proof2cic [] p
-		 | _ -> prerr_endline "7a"; assert false) patterns)
+                 | _ -> prerr_endline "7a"; assert false) patterns)
       | Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns ->           C.MutCase
             (UriManager.uri_of_string uri,
              int_of_string notype, deannotate ty, deannotate te,
              List.map 
                (function 
                    (Con.ArgProof p) -> proof2cic [] p
-		 | _ -> prerr_endline "7a"; assert false) patterns) 
+                 | _ -> prerr_endline "7a"; assert false) patterns) 
       | _ -> (prerr_endline "7"; assert false))
     else if (conclude.Con.conclude_method = "Apply") then
       let cargs = (args2cic premise_env conclude.Con.conclude_args) in
@@ -207,10 +210,10 @@ let proof2cic deannotate p =
                with Not_found -> 
                   prerr_endline ("Not_found in arg2cic: premise " ^ (match prem.Con.premise_binder with None -> "previous" | Some p -> p) ^ ", xref=" ^ prem.Con.premise_xref);
                   raise Not_found))
-      | Con.Term t -> 
-          deannotate t
-      | Con.ArgProof p ->
-          proof2cic [] p (* empty! *)
+      | Con.Lemma lemma ->
+         CicUtil.term_of_uri (UriManager.uri_of_string lemma.Con.lemma_uri)
+      | Con.Term t -> deannotate t
+      | Con.ArgProof p -> proof2cic [] p (* empty! *)
       | Con.ArgMethod s -> raise TO_DO
 
 in proof2cic [] p
@@ -225,7 +228,7 @@ let cobj2obj deannotate (id,params,metasenv,obj) =
       (match metasenv with
           None ->
            Cic.Constant
-            (id, Some (proof2cic deannotate bo), deannotate ty, params)
+            (id, Some (proof2cic deannotate bo), deannotate ty, params, [])
         | Some metasenv' ->
            let metasenv'' =
             List.map
@@ -233,22 +236,23 @@ let cobj2obj deannotate (id,params,metasenv,obj) =
                let canonical_context' =
                 List.map
                  (function
-                     _,None -> None
-                   | _,Some (`Declaration d) 
-                   | _,Some (`Hypothesis d) ->
+                     None -> None
+                   | Some (`Declaration d) 
+                   | Some (`Hypothesis d) ->
                      (match d with
                         {K.dec_name = Some n ; K.dec_type = t} ->
                           Some (Cic.Name n, Cic.Decl (deannotate t))
                       | _ -> assert false)
-                   | _,Some (`Definition d) ->
+                   | Some (`Definition d) ->
                       (match d with
                           {K.def_name = Some n ; K.def_term = t} ->
-                            Some (Cic.Name n, Cic.Def (deannotate t))
+                            Some (Cic.Name n, Cic.Def ((deannotate t),None))
                         | _ -> assert false)
-                   | _,Some (`Proof d) ->
+                   | Some (`Proof d) ->
                       (match d with
                           {K.proof_name = Some n } ->
-                            Some (Cic.Name n, Cic.Def (proof2cic deannotate d))
+                            Some (Cic.Name n,
+                              Cic.Def ((proof2cic deannotate d),None))
                         | _ -> assert false)
                  ) canonical_context
                in
@@ -256,7 +260,8 @@ let cobj2obj deannotate (id,params,metasenv,obj) =
              ) metasenv'
            in
             Cic.CurrentProof
-             (id, metasenv'', proof2cic deannotate bo, deannotate ty, params))
+             (id, metasenv'', proof2cic deannotate bo, deannotate ty, params,
+              []))
   | _ -> raise ToDo
 ;;