bugfix: use only baseuri in uri part of MutInd and MutConstruct

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index 36c266ba7b7054ebbfec0941c6e4a48d13262219..3f61565401adf41cbbf3bd84e4c87ac82bcc29f4 100644 (file)
--- 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