?(localise=fun _ -> Stdpp.dummy_loc)
~look_for_coercion metasenv subst context term expty
=
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context term);
let force_ty metasenv subst context orig t infty expty =
(*D*)inside 'F'; try let rc =
match expty with
let _, _, arity, cl = List.nth itl tyno in
let constructorsno = List.length cl in
let _, metasenv, args =
- NCicMetaSubst.saturate metasenv context arity 0 in
+ NCicMetaSubst.saturate metasenv subst context arity 0 in
let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
let metasenv, subst, term, _ =
typeof_aux metasenv subst context (Some ind) term in