From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 21 Oct 2004 15:53:25 +0000 (+0000)
Subject: bugfix: use only baseuri in uri part of MutInd and MutConstruct
X-Git-Tag: V_0_0_10~56
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d491d2def96ddd1c27299ad0fa3d0cae39aa45ce;p=helm.git

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 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