From 24be58b2d60442e197293f3704d4dff9961e6046 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
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