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 ->
(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
;;