From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 13 May 2008 17:07:07 +0000 (+0000)
Subject: Never commit before trying to compile... stupid typo fixed.
X-Git-Tag: make_still_working~5222
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dfc88cb4e7d0dca81cabe418d2c732cd22166726;p=helm.git

Never commit before trying to compile... stupid typo fixed.
---

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index 5faab078f..6bc725033 100644
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -127,11 +127,10 @@ let _ =
       NCicTypeChecker.typecheck_obj o
     with 
     | NCicTypeChecker.AssertFailure s 
-    | NCicTypeChecker.TypeCheckerFailure s as e -> 
+    | NCicTypeChecker.TypeCheckerFailure s
+    | NCicEnvironment.ObjectNotFound s as e -> 
        prerr_endline ("######### " ^ Lazy.force s);
        if not ignore_exc then raise e
-    | NCicEnvironment.Object_not_found s -> 
-       prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s)
     )
     alluris;
   NCicEnvironment.invalidate ();