]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/check.ml
nuri_of_ouri, ouri_of_nuri, reference_of_ouri, ouri_of_reference moved
[helm.git] / helm / software / components / ng_kernel / check.ml
index d0c18e6a7642afbb787862002c0e575118e4ed9a..9fefb3c99eb40210c7aee9f9043f8427b4d493c7 100644 (file)
@@ -133,7 +133,7 @@ let _ =
   prerr_endline "ranked....";
   HExtlib.profiling_enabled := false;
   List.iter (fun uu ->
-    let uu= NUri.nuri_of_ouri uu in
+    let uu= OCic2NCic.nuri_of_ouri uu in
     indent := 0;
     let o = NCicLibrary.get_obj uu in
     try 
@@ -156,7 +156,7 @@ let _ =
   let prima = Unix.gettimeofday () in
   List.iter 
     (fun u ->
-       let u= NUri.nuri_of_ouri u in
+       let u= OCic2NCic.nuri_of_ouri u in
       indent := 0;
       NCicTypeChecker.typecheck_obj (NCicLibrary.get_obj u))
     alluris;