- Lemma added to the list of proof arguments

[helm.git] / helm / ocaml / cic_omdoc / content2cic.ml

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index d25d7942595f8b20348b1dc37596516f678f3dfd..b1151c792400ea6f4986a82040b03eb65b965d5b 100644 (file)
--- 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 ->