From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 4 Apr 2008 13:07:36 +0000 (+0000)
Subject: added some printings and catched more exceptions
X-Git-Tag: make_still_working~5449
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cdbdd1610eec11df04e6b8484f9942f45e0403f0;p=helm.git

added some printings and catched more exceptions
---

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index 39e80cca2..a1d2a7ccb 100644
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -11,10 +11,13 @@ let _ =
   let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph u in
   let l = OCic2NCic.convert_obj u o in
   List.iter 
-    (fun o ->
+    (fun (u,_,_,_,_ as o) ->
+       prerr_endline ("CHECK: " ^ NUri.string_of_uri u);
        try NCicTypeChecker.typecheck_obj o
        with 
        | NCicTypeChecker.AssertFailure s 
-       | NCicTypeChecker.TypeCheckerFailure s -> prerr_endline (Lazy.force s))
+       | NCicTypeChecker.TypeCheckerFailure s -> prerr_endline (Lazy.force s)
+       (*| CicEnvironment.Object_not_found s -> 
+           prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s)*))
     l
 ;;