| NCicUnification.Uncertain _ as exc -> first exc tl
in
first exc
- (NCicCoercion.look_for_coercion
- rdb.NRstatus.coerc_db metasenv subst context infty expty)
+ (NCicCoercion.look_for_coercion rdb metasenv subst context infty expty)
and force_to_sort rdb metasenv subst context t orig_t localise ty =
match NCicReduction.whd ~subst context ty with
let typeof_obj
rdb ?(localise=fun _ -> Stdpp.dummy_loc) (uri,height,metasenv,subst,obj)
=
-prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj));
let check_type metasenv subst context (ty as orig_ty) = (* XXX fattorizza *)
let metasenv, subst, ty, sort =
typeof rdb ~localise metasenv subst context ty None
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 =