X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcontent2cic.ml;h=b1151c792400ea6f4986a82040b03eb65b965d5b;hb=414dc18cdbc1f431758cfce79b0b7827e2419d39;hp=d25d7942595f8b20348b1dc37596516f678f3dfd;hpb=22a8ad8462e81ad68d8016a009fa8003bd52a66f;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index d25d79425..b1151c792 100644
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -207,6 +207,9 @@ 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 lemma.Con.lemma_uri)
       | Con.Term t -> 
           deannotate t
       | Con.ArgProof p ->