- let metasenv,_,instance,_ =
- NCicMetaSubst.mk_meta metasenv context_of_args `Term in
- let meta_applied = mk_appl (instance::List.rev processed_args) in
-let metasenv,subst,_,_ =
- !refiner_typeof ((rdb :> NRstatus.status)#set_coerc_db NCicCoercion.empty_db) metasenv subst context_of_args meta_applied None
-in
- let metasenv,subst =
- unify rdb true metasenv subst context_of_args meta_applied ty in
- let telescopic_ty = NCicSubstitution.lift n instance in
- let telescopic_ty =
- mk_appl (telescopic_ty :: mk_irl (List.length processed_args)) in