| C.Rel m when m <= k || m > nn+k -> ()
| C.Rel m ->
(try match List.nth context (m-1-k) with
- | _,C.Def (bo,_) -> aux (n-m) () bo
+ | _,C.Def (bo,_) -> aux 0 () (S.lift status (m-k) bo)
| _ -> ()
with Failure _ -> assert false)
| C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
| 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)