match bo with
| Some bo ->
let metasenv, subst, bo, ty =
- typeof rdb ~localise metasenv subst [] bo (Some ty)
- in
+ typeof rdb ~localise metasenv subst [] bo (Some ty) in
let height = (* XXX recalculate *) height in
metasenv, subst, Some bo, ty, height
| None -> metasenv, subst, None, ty, 0
List.fold_left
(fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) ->
let metasenv, subst, ty, _ = check_type metasenv subst [] ty in
- let dbo = NCicTypeChecker.debruijn uri len [] bo in
+ let dbo = NCicTypeChecker.debruijn uri len [] ~subst bo in
let localise = relocalise localise dbo bo in
(name,C.Decl ty)::types,
metasenv, subst, (relevance,name,k,ty,dbo,localise)::fl
let k_relev =
try snd (HExtlib.split_nth leftno k_relev)
with Failure _ -> k_relev in
- let te = NCicTypeChecker.debruijn uri len [] te in
+ let te = NCicTypeChecker.debruijn uri len [] ~subst te in
let metasenv, subst, te, _ = check_type metasenv subst tys te in
let context,te = NCicReduction.split_prods ~subst tys leftno te in
let _,chopped_context_rev =
raise
(RefineFailure
(lazy (localise te,
- "Non positive occurence in " ^ NUri.string_of_uri uri)))
+ "Non positive occurence in " ^
+ NCicPp.ppterm ~metasenv ~subst ~context te)))
else
let relsno = List.length itl + leftno in
let te =