From 24be58b2d60442e197293f3704d4dff9961e6046 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 22 Oct 2004 12:35:15 +0000 Subject: [PATCH] no longer depends on MQueryMisc --- helm/ocaml/cic_omdoc/content2cic.ml | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml index 2cc72933b..bf80a5939 100644 --- a/helm/ocaml/cic_omdoc/content2cic.ml +++ b/helm/ocaml/cic_omdoc/content2cic.ml @@ -210,15 +210,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 - (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 lemma.Con.lemma_uri + | Con.Term t -> deannotate t + | Con.ArgProof p -> proof2cic [] p (* empty! *) | Con.ArgMethod s -> raise TO_DO in proof2cic [] p -- 2.39.2