]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicUtil.ml
more strings to UriManager.uri
[helm.git] / helm / ocaml / cic / cicUtil.ml
index a0b03527878f3754325c852f74f1170f78077fd8..a3649ca36ed312874b333d39696a9a2c5bbf8ef0 100644 (file)
@@ -138,8 +138,8 @@ let rec is_meta_closed =
 let xpointer_RE = Str.regexp "\\([^#]+\\)#xpointer(\\(.*\\))"
 let slash_RE = Str.regexp "/"
 
-let term_of_uri s =
-  let uri = UriManager.uri_of_string s in
+let term_of_uri uri =
+  let s = UriManager.string_of_uri uri in
   try
     (if String.sub s (String.length s - 4) 4 = ".con" then
       Cic.Const (uri, [])
@@ -163,12 +163,14 @@ let term_of_uri s =
 
 let uri_of_term = function
   | Cic.Const (uri, [])
-  | Cic.Var (uri, []) -> UriManager.string_of_uri uri
+  | Cic.Var (uri, []) -> uri
   | Cic.MutInd (baseuri, tyno, []) ->
-      sprintf "%s#xpointer(1/%d)" (UriManager.string_of_uri baseuri) (tyno + 1)
+     UriManager.uri_of_string
+      (sprintf "%s#xpointer(1/%d)" (UriManager.string_of_uri baseuri) (tyno+1))
   | Cic.MutConstruct (baseuri, tyno, consno, []) ->
-      sprintf "%s#xpointer(1/%d/%d)" (UriManager.string_of_uri baseuri)
-        (tyno + 1) consno
+     UriManager.uri_of_string
+      (sprintf "%s#xpointer(1/%d/%d)" (UriManager.string_of_uri baseuri)
+        (tyno + 1) consno)
   | _ -> raise (Invalid_argument "uri_of_term")
 
 let select ~term ~context =