- let metasenv,_,instance,_ =
- NCicMetaSubst.mk_meta metasenv context_of_args `Term in
- let meta_applied =
- NCicUntrusted.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 =
- NCicUntrusted.mk_appl
- telescopic_ty (mk_irl (List.length processed_args)) in