X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Flibrary%2FlibraryClean.ml;h=00f2c4ef0f168e13eecc6c49c701acd502974aae;hb=5dd5b3f6cd990d4d126b44c092e1df7f86c506d4;hp=a7a3d7345886027bec83229911b6a4928aa84ac0;hpb=a58d25c192ff13ecee2cb92f07ee6f1cbe5219b5;p=helm.git

diff --git a/helm/ocaml/library/libraryClean.ml b/helm/ocaml/library/libraryClean.ml
index a7a3d7345..00f2c4ef0 100644
--- a/helm/ocaml/library/libraryClean.ml
+++ b/helm/ocaml/library/libraryClean.ml
@@ -122,10 +122,10 @@ let close_uri_list uri_to_remove =
   in
   uri_to_remove, depend
 
-let rec close_using_db uris next =
+let rec close_db uris next =
   match next with
   | [] -> uris
-  | l -> let uris, next = close_uri_list l in close_using_db uris next @ uris
+  | l -> let uris, next = close_uri_list l in close_db uris next @ uris
   
 let cleaned_no = ref 0;;
 
@@ -145,7 +145,7 @@ let moo_root_dir = lazy (
   String.sub url 7 (String.length url - 7)  (* remove heading "file:///" *)
 )
 
-let close_using_moos buris =
+let close_nodb buris =
   let rev_deps = Hashtbl.create 97 in
   let all_moos =
     HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo")
@@ -153,11 +153,11 @@ let close_using_moos buris =
   in
   List.iter
     (fun path -> 
-      let _, metadata = GrafiteMarshal.load_moo ~fname:path in
+      let metadata = LibraryNoDb.load_metadata ~fname:path in
       let baseuri_of_current_moo = 
         let rec aux = function 
           | [] -> assert false
-          | GrafiteAst.Baseuri buri::_ -> buri
+          | LibraryNoDb.Baseuri buri::_ -> buri
           | _ :: tl -> aux tl
         in
         aux metadata
@@ -165,7 +165,7 @@ let close_using_moos buris =
       let deps = 
         HExtlib.filter_map 
           (function 
-          | GrafiteAst.Dependency buri -> Some buri
+          | LibraryNoDb.Dependency buri -> Some buri
           | _ -> None ) 
         metadata
       in
@@ -198,9 +198,9 @@ let clean_baseuris ?(verbose=true) ~basedir buris =
     List.iter debug_prerr buris; 
   let l = 
     if Helm_registry.get_bool "db.nodb" then
-      close_using_moos buris
+      close_nodb buris
     else
-      close_using_db [] buris 
+      close_db [] buris 
   in
   let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
   let l = List.map UriManager.uri_of_string l in