]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/content2cic.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_omdoc / content2cic.ml
index fdc2cea1cee300573c739dfe597ea46896c52242..339492d1985317911dad12a0890d5a89d62fea25 100644 (file)
@@ -210,7 +210,8 @@ 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 -> CicUtil.term_of_uri lemma.Con.lemma_uri
+      | 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