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

diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml
index a1c24d9c6..50407ac7c 100644
--- a/helm/ocaml/metadata/metadataExtractor.ml
+++ b/helm/ocaml/metadata/metadataExtractor.ml
@@ -56,7 +56,7 @@ module OrderedMetadata =
   end
 
 module MetadataSet = Set.Make (OrderedMetadata)
-module StringSet = Set.Make (String)
+module UriManagerSet = UriManager.UriSet
 
 module S = MetadataSet
 
@@ -130,17 +130,17 @@ let compute_term pos term =
           (fun set term -> aux (next_pos pos) set term)
           set tl
     | Cic.Const (uri, subst) ->
-        let set = S.add (`Obj (string_of_uri uri, pos)) set 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.MutInd (uri, typeno, subst) ->
-        let uri = UriManager.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 = UriManager.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
@@ -241,13 +241,13 @@ let compute_metas term =
 let compute_type pos uri typeno (name, _, ty, constructors) =
   let consno = ref 0 in
   let type_metadata =
-    (UriManager.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 = UriManager.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
@@ -268,14 +268,14 @@ let compute (pos:position) ~body ~ty =
     S.fold
       (fun metadata uris ->
         match metadata with
-        | `Obj (uri, _) -> StringSet.add uri uris
+        | `Obj (uri, _) -> UriManagerSet.add uri uris
         | _ -> uris)
-      type_metadata StringSet.empty
+      type_metadata UriManagerSet.empty
   in
   S.union
     (S.filter
       (function
-        | `Obj (uri, _) when StringSet.mem uri uris -> false
+        | `Obj (uri, _) when UriManagerSet.mem uri uris -> false
         | _ -> true)
       body_metadata)
     type_metadata
@@ -321,7 +321,7 @@ let compute_obj uri =
           S.empty
           params
       in
-      [ UriManager.string_of_uri uri, 
+      [ uri, 
         UriManager.name_of_uri uri,
         S.union metadata var_metadata ]
   | Cic.InductiveDefinition (types, params, _, _) ->