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

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index 2cc72933b..339492d19 100644
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -210,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
@@ -233,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
@@ -265,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
 ;;