X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2Fcheck.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2Fcheck.ml;h=71ba8ddc284720f3ec8bed7fa0ed08c34b41d6d6;hb=f7101ffe7045c53dde6e1371005f9ceac1852826;hp=4f99dd05783aaf1554a0699bb9da1f48c66b89c7;hpb=a3b43762ca9cfb746933dcd991bfc363b5fdd9b7;p=helm.git

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index 4f99dd057..71ba8ddc2 100644
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -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 ();