X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=b60734508b46b5a6fe5687086ce7a8e45bfd640c;hb=73966e3e9fd17155ca67e6b4a32f52225cea9d3c;hp=e334861cbf9c0482f02e8e7401f6fb24e8b7f4c6;hpb=5af5db14a2bb7583ae1b8eaaf18ad26a06e3d892;p=helm.git

diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml
index e334861cb..b60734508 100644
--- a/matita/components/ng_kernel/nCicTypeChecker.ml
+++ b/matita/components/ng_kernel/nCicTypeChecker.ml
@@ -391,7 +391,7 @@ let rec typeof (status:#NCic.status) ~subst ~metasenv context term =
          match List.nth context (n - 1) with
          | (_,C.Decl ty) -> S.lift status n ty
          | (_,C.Def (_,ty)) -> S.lift status n ty
-        with Failure _ -> 
+        with Failure _ | Invalid_argument _ -> 
           raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
             ^" under: " ^ status#ppcontext ~metasenv ~subst context))))
     | C.Sort s -> 
@@ -1329,7 +1329,7 @@ let typecheck_obj status (uri,height,metasenv,subst,kind) =
              (guarded_by_constructors status ~subst ~metasenv types bo r_uri r_len len)
              then
                raise (TypeCheckerFailure
-                (lazy "CoFix: not guarded by constructors"))
+                (lazy ("CoFix: not guarded by constructors: " ^ status#ppobj (uri,height,metasenv,subst,kind))))
         ) fl dfl
 ;;