]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/check.ml
Reverting to the previous version some files which weren't intended to be
[helm.git] / helm / software / components / ng_kernel / check.ml
index 4f99dd05783aaf1554a0699bb9da1f48c66b89c7..71ba8ddc284720f3ec8bed7fa0ed08c34b41d6d6 100644 (file)
@@ -12,8 +12,7 @@
 (* $Id$ *)
 
 let debug = true
-let ignore_exc = true
-let ignore_exc_new_typing = true
+let ignore_exc = false
 let rank_all_dependencies = false
 let trust_environment = false
 
@@ -186,14 +185,7 @@ let _ =
     (fun u ->
        let u= OCic2NCic.nuri_of_ouri u in
       indent := 0;
-      try NCicTypeChecker.typecheck_obj (NCicLibrary.get_obj u)
-      with 
-      | NCicTypeChecker.AssertFailure s
-      | NCicTypeChecker.TypeCheckerFailure s
-      | NCicEnvironment.ObjectNotFound s
-      | NCicEnvironment.BadDependency s as e ->
-         prerr_endline ("######### " ^ Lazy.force s);
-         if not ignore_exc_new_typing then raise e)
+      NCicTypeChecker.typecheck_obj (NCicLibrary.get_obj u))
     alluris;
   let dopo = Unix.gettimeofday () in
   Gc.compact ();