- metasenv, subst, bo
- | (arg,ty)::tail ->
- pp(lazy("arg{ " ^
- NCicPp.ppterm ~metasenv ~subst ~context:context_of_args arg ^ " : " ^
- NCicPp.ppterm ~metasenv ~subst ~context:context_of_args ty));
- let metasenv, subst, telescopic_ty =
- if processed_args = [] then metasenv, subst, ty else
- let _ = pp(lazy("delift")) in
- delift_type_wrt_terms rdb metasenv subst context
- (NCicSubstitution.lift n ty)
- (List.map (NCicSubstitution.lift n) (List.rev processed_args))
- in
- pp(lazy("arg} "^NCicPp.ppterm ~metasenv ~subst ~context telescopic_ty));
- let name = "HBeta"^string_of_int n in
- 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)
- in
- pp(lazy("LAMBDA_INTROS{ " ^
- NCicPp.ppterm ~metasenv ~subst ~context t ^ ":" ^
- NCicPp.ppterm ~metasenv ~subst ~context tty ^ " over " ^
- String.concat "," (List.map (NCicPp.ppterm ~metasenv ~subst ~context)args)));
- let rc = mk_lambda metasenv subst context 0 [] argsty in
- pp(lazy("LAMBDA_INTROS}"));
- rc
-
-and instantiate rdb test_eq_only metasenv subst context n lc t swap =
+ metasenv, bo
+ | _ ->
+ (match NCicReduction.whd ~subst context ty with
+ C.Prod (n,so,ta) ->
+ let metasenv,bo =
+ lambda_intros rdb metasenv subst
+ ((n,C.Decl so)::context) (argsno - 1) ta
+ in
+ metasenv,C.Lambda (n,so,bo)
+ | _ -> assert false)
+;;
+
+let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =