-and delift_term_wrt_terms rdb metasenv subst context t args =
- let metasenv, _, instance, _ =
- NCicMetaSubst.mk_meta metasenv context `Term in
- let meta_applied = NCicUntrusted.mk_appl instance args in
- let metasenv,subst,meta_applied,_ =
- !refiner_typeof ((rdb:> NRstatus.status)#set_coerc_db NCicCoercion.empty_db)
- metasenv subst context meta_applied None
+and delift_type_wrt_terms rdb metasenv subst context t args =
+ let (metasenv, subst), t =
+ try
+ NCicMetaSubst.delift
+ ~unify:(fun m s c t1 t2 ->
+ let ind = !indent in
+ let res =
+ try Some (unify rdb false m s c t1 t2 )
+ with UnificationFailure _ | Uncertain _ -> None
+ in
+ indent := ind; res)
+ metasenv subst context 0 (0,NCic.Ctx (args @
+ List.rev (mk_irl (List.length context)))) t
+ with NCicMetaSubst.MetaSubstFailure _ -> (metasenv, subst), t