]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaclean.ml
1. matitaEngine splitted into disambiguation (now in grafite_parser) and
[helm.git] / helm / matita / matitaclean.ml
index 807f545258ff899ac98eaa226b8fd3352b14ad18..b8c2bb4c28cc66c9b985931efcf3cb774dca10ec 100644 (file)
@@ -55,7 +55,7 @@ let main () =
               UM.buri_of_uri (UM.uri_of_string suri)
             with UM.IllFormedUri _ ->
               files_to_remove := suri :: !files_to_remove;
-              let u = MatitaMisc.baseuri_of_file suri in
+              let u = GrafiteMisc.baseuri_of_file suri in
               if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin
                 HLog.error (sprintf "File %s defines a bad baseuri: %s"
                   suri u);
@@ -67,7 +67,7 @@ let main () =
         files);
   LibraryClean.clean_baseuris ~basedir !uris_to_remove;
   let moos =
-   List.map (MatitaMisc.obj_file_of_script ~basedir) !files_to_remove
+   List.map (GrafiteMisc.obj_file_of_script ~basedir) !files_to_remove
   in
    List.iter HExtlib.safe_remove moos