- ng_kernel: catched Invalid_argument "List.nth" in typeof of Rel i (raied when i...

[helm.git] / matita / components / ng_kernel / nCicTypeChecker.ml

diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml
index 343be2607277b7bbab8e4bd0523fc35d9d7d0069..6871dc6ee3775ba4983f88f48ac5757c59ed6ec1 100644 (file)
--- 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 -> 
@@ -1131,7 +1131,7 @@ and get_relevance status ~metasenv ~subst context t args =
               | C.Sort C.Prop ->
                   false::(aux context new_ty tl)
               | C.Sort _
-                   | C.Meta _ -> true::(aux context new_ty tl)
+              | C.Meta _ -> true::(aux context new_ty tl)
               | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
                      "Prod: the type %s of the source of %s is not a sort" 
                       (status#ppterm ~subst ~metasenv ~context sort)