]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/matitadep.ml
urimanager removed
[helm.git] / matita / matita / matitadep.ml
index 73ce0cd8184b7277cf240aef69f839301351c968..3156783071755b5fd6cf0a7c797948b5ee329033 100644 (file)
@@ -28,7 +28,6 @@
 module S = Set.Make (String)
 
 module GA = GrafiteAst 
-module U = UriManager
 module HR = Helm_registry
 
 let print_times msg = 
@@ -104,7 +103,7 @@ let main () =
       HLog.error ("possibly incorrect verbatim URIs in the .ma file.");
       None
   in
-  let buri alias = U.buri_of_uri (U.uri_of_string alias) in
+  let buri alias = NUri.baseuri_of_uri (NUri.uri_of_string alias) in
   let resolve alias current_buri =
     let buri = buri alias in
     if buri <> current_buri then Some buri else None 
@@ -190,7 +189,7 @@ let main () =
       List.iter 
        (function
          | DependenciesParser.UriDep uri      ->
-            let uri = UriManager.string_of_uri uri in
+            let uri = NUri.string_of_uri uri in
            handle_uri uri 
          | DependenciesParser.InlineDep path  ->
            if Librarian.is_uri path