]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_kernel/nCicTypeChecker.ml
- ng_kernel: catched Invalid_argument "List.nth" in typeof of Rel i (raied when i...
[helm.git] / matita / components / ng_kernel / nCicTypeChecker.ml
index e334861cbf9c0482f02e8e7401f6fb24e8b7f4c6..6871dc6ee3775ba4983f88f48ac5757c59ed6ec1 100644 (file)
@@ -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 ->