match List.nth context (n - 1) with
| (_,C.Decl ty) -> S.lift status n ty
| (_,C.Def (_,ty)) -> S.lift status n ty
match List.nth context (n - 1) with
| (_,C.Decl ty) -> S.lift status n ty
| (_,C.Def (_,ty)) -> S.lift status n ty
raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
^" under: " ^ status#ppcontext ~metasenv ~subst context))))
| C.Sort s ->
raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
^" under: " ^ status#ppcontext ~metasenv ~subst context))))
| C.Sort s ->
| _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
"Prod: the type %s of the source of %s is not a sort"
(status#ppterm ~subst ~metasenv ~context sort)
| _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
"Prod: the type %s of the source of %s is not a sort"
(status#ppterm ~subst ~metasenv ~context sort)