| 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