]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/check.ml
Fix name capture in cofix.
[helm.git] / helm / software / components / ng_kernel / check.ml
index 918a4ddb3590d7ce33df4ebb7025d4b621606350..d2f54612222e235fb9a46fb294c2f3d3de86189b 100644 (file)
@@ -48,9 +48,10 @@ let _ =
     | CicEnvironment.Object_not_found s -> 
                     prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s);
     )
-  alluris;
+    alluris;
   NCicEnvironment.invalidate ();
   Gc.compact ();
+  prerr_endline "typechecking, first with the new and then with the old kernel";
   let prima = Unix.gettimeofday () in
   List.iter 
     (fun u -> NCicTypeChecker.typecheck_obj (snd (NCicEnvironment.get_obj u)))
@@ -58,7 +59,7 @@ let _ =
   let dopo = Unix.gettimeofday () in
   Gc.compact ();
   let dopo2 = Unix.gettimeofday () in
-  Printf.eprintf "NEW typing: %3.2f, gc: %3.2f\n" (dopo -. prima) (dopo2 -.  dopo);
+  Printf.eprintf "NEW typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -.  dopo);
   CicEnvironment.invalidate ();
   let alluris = List.map NUri.ouri_of_nuri alluris in
   Gc.compact ();
@@ -67,5 +68,5 @@ let _ =
   let dopo = Unix.gettimeofday () in
   Gc.compact ();
   let dopo2 = Unix.gettimeofday () in
-  Printf.eprintf "OLD typing: %3.2f, gc: %3.2f\n" (dopo -. prima) (dopo2 -. dopo)
+  Printf.eprintf "OLD typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -. dopo)
 ;;