let pp s =
prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
;;
-let pp _ = ();;
+let pp _ = ();;
let ppcontext = NCicPp.ppcontext;;
let ppmetasenv = NCicPp.ppmetasenv;;
in
metasenv, subst, bo
| (arg,ty)::tail ->
+ let metasenv, subst, telescopic_ty =
+ delift_term_wrt_terms rdb metasenv subst context_of_args ty
+ (List.rev processed_args)
+ in
let name = "HBeta"^string_of_int n in
- 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
let metasenv, subst, bo =
mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1)
(arg::processed_args) tail
| UnificationFailure _ -> raise (UnificationFailure msg)
| Uncertain _ -> raise exn
(*D*) in outside(); rc with exn -> outside (); raise exn
+
+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
+ in
+ let metasenv, subst =
+ unify rdb true metasenv subst context meta_applied t in
+ let t = NCicSubstitution.lift (List.length args) instance in
+ let t = NCicUntrusted.mk_appl t (mk_irl (List.length args)) in
+ metasenv, subst, t
;;
+
let unify rdb ?(test_eq_only=false) =
indent := "";
unify rdb test_eq_only;;