From: Claudio Sacerdoti Coen Date: Fri, 25 Jul 2003 11:14:42 +0000 (+0000) Subject: Lemma generated wrong URIs (again). Fixed. X-Git-Tag: LucaOK~32 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f9fb6aea5ebbb04018ce2b9e4a395339b58d8ff9;p=helm.git Lemma generated wrong URIs (again). Fixed. --- diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml index b1151c792..644f55920 100644 --- a/helm/ocaml/cic_omdoc/content2cic.ml +++ b/helm/ocaml/cic_omdoc/content2cic.ml @@ -177,14 +177,14 @@ let proof2cic deannotate p = List.map (function Con.ArgProof p -> proof2cic [] p - | _ -> prerr_endline "7a"; assert false) patterns) + | _ -> prerr_endline "7a"; assert false) patterns) | Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns -> C.MutCase (UriManager.uri_of_string uri, int_of_string notype, deannotate ty, deannotate te, List.map (function (Con.ArgProof p) -> proof2cic [] p - | _ -> prerr_endline "7a"; assert false) patterns) + | _ -> prerr_endline "7a"; assert false) patterns) | _ -> (prerr_endline "7"; assert false)) else if (conclude.Con.conclude_method = "Apply") then let cargs = (args2cic premise_env conclude.Con.conclude_args) in @@ -208,8 +208,10 @@ let proof2cic deannotate p = 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) + 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 ->