- let ty = NCicSubstitution.lift n ty in
- let metasenv, bo = mk_lambda ((name,NCic.Decl ty)::context) (n+1) tail in
- metasenv, NCic.Lambda (name, ty, bo)
+ 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
+prerr_endline ("########################## LI1: " ^ NCicPp.ppterm ~metasenv ~subst ~context:context_of_args meta_applied ^ " vs " ^ NCicPp.ppterm ~metasenv ~subst ~context:context_of_args ty);
+prerr_endline (NCicPp.ppcontext ~metasenv ~subst context_of_args);
+prerr_endline (NCicPp.ppmetasenv metasenv ~subst);
+ let metasenv,subst =
+ unify rdb true metasenv subst context_of_args meta_applied ty in
+prerr_endline "UNIFY FINITA";
+ let telescopic_ty = NCicSubstitution.lift n instance in
+ let telescopic_ty =
+ mk_appl (telescopic_ty :: mk_irl (List.length processed_args)) in
+prerr_endline ("########################## LI: " ^ NCicPp.ppterm ~metasenv ~subst ~context telescopic_ty);
+ let metasenv, subst, bo =
+ mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1)
+ (arg::processed_args) tail
+ in
+ metasenv, subst, NCic.Lambda (name, telescopic_ty, bo)