X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataExtractor.ml;h=50407ac7c923d7ff94116fe5aa98976e38f3f6f5;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=5a7522b90eb6f5c3c017bcecd15d915f5d21d8ac;hpb=a7b90d2494f7d580faa54ecd2835bd4649129763;p=helm.git

diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml
index 5a7522b90..50407ac7c 100644
--- a/helm/ocaml/metadata/metadataExtractor.ml
+++ b/helm/ocaml/metadata/metadataExtractor.ml
@@ -72,9 +72,6 @@ let var_has_body uri =
   | Cic.Variable (_, Some body, _, _, _), _ -> true
   | _ -> false
 
-let string_of_uriref s =
- UriManager.uri_of_string (UriManager.string_of_uriref s)
-
 let compute_term pos term =
   let rec aux (pos: position) set = function
     | Cic.Var (uri, subst) when var_has_body uri ->
@@ -138,12 +135,12 @@ let compute_term pos term =
           (fun set (_, term) -> aux (next_pos pos) set term)
           set subst
     | Cic.MutInd (uri, typeno, subst) ->
-        let uri = string_of_uriref (uri, [typeno]) in
+        let uri = UriManager.uri_of_uriref uri typeno None in
         let set = S.add (`Obj (uri, pos)) set in
         List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
           set subst
     | Cic.MutConstruct (uri, typeno, consno, subst) ->
-        let uri = string_of_uriref (uri, [typeno; consno]) in
+        let uri = UriManager.uri_of_uriref uri typeno (Some consno) in
         let set = S.add (`Obj (uri, pos)) set in
         List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
           set subst
@@ -244,13 +241,13 @@ let compute_metas term =
 let compute_type pos uri typeno (name, _, ty, constructors) =
   let consno = ref 0 in
   let type_metadata =
-    (string_of_uriref (uri, [typeno]), name, (compute_term pos ty))
+    (UriManager.uri_of_uriref uri typeno None, name, (compute_term pos ty))
   in
   let constructors_metadata =
     List.map
       (fun (name, term) ->
         incr consno;
-        let uri = string_of_uriref (uri, [typeno; !consno]) in
+        let uri = UriManager.uri_of_uriref uri typeno (Some !consno) in
         (uri, name, (compute_term pos term)))
       constructors
   in