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

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index ed62e254c..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
@@ -207,15 +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.Lemma lemma -> 
-          MQueryMisc.term_of_cic_textual_parser_uri 
-           (MQueryMisc.cic_textual_parser_uri_of_string
-            (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
-              lemma.Con.lemma_uri))
-      | 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
@@ -230,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
@@ -262,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
 ;;