]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataExtractor.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / metadata / metadataExtractor.ml
index 5a7522b90eb6f5c3c017bcecd15d915f5d21d8ac..50407ac7c923d7ff94116fe5aa98976e38f3f6f5 100644 (file)
@@ -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