From d491d2def96ddd1c27299ad0fa3d0cae39aa45ce Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 21 Oct 2004 15:53:25 +0000 Subject: [PATCH] bugfix: use only baseuri in uri part of MutInd and MutConstruct --- helm/ocaml/cic/cicUtil.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index 36c266ba7..3f6156540 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -142,7 +142,7 @@ let meta_closed t = in try visit_t (fun x -> x) () t; false with Exit -> true -let xpointer_RE = Str.regexp "[^#]+#xpointer(\\(.*\\))" +let xpointer_RE = Str.regexp "\\([^#]+\\)#xpointer(\\(.*\\))" let slash_RE = Str.regexp "/" let term_of_uri s = @@ -155,11 +155,13 @@ let term_of_uri s = else if not (Str.string_match xpointer_RE s 0) then raise (UriManager.IllFormedUri s) else - (match Str.split slash_RE (Str.matched_group 1 s) with - | [_; tyno] -> Cic.MutInd (uri, int_of_string tyno - 1, []) + let (baseuri,xpointer) = (Str.matched_group 1 s, Str.matched_group 2 s) in + let baseuri = UriManager.uri_of_string baseuri in + (match Str.split slash_RE xpointer with + | [_; tyno] -> Cic.MutInd (baseuri, int_of_string tyno - 1, []) | [_; tyno; consno] -> Cic.MutConstruct - (uri, int_of_string tyno - 1, int_of_string consno, []) + (baseuri, int_of_string tyno - 1, int_of_string consno, []) | _ -> raise Exit)) with | Exit -- 2.39.2