- | []->metasenv, subst, NCicUntrusted.mk_appl he (List.rev args_so_far), ty_he
+ | [] ->
+ let res = NCicUntrusted.mk_appl he (List.rev args_so_far) in
+ pp(lazy("FORCE FINAL APPL: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context res ^
+ " of type " ^ NCicPp.ppterm ~metasenv ~subst ~context ty_he
+ ^ " to type " ^ match expty with None -> "None" | Some x ->
+ NCicPp.ppterm ~metasenv ~subst ~context x));
+ (* whatever the term is, we force the type. in case of ((Lambda..) ?...)
+ * the application may also be a lambda! *)
+ force_ty false false metasenv subst context orig_t res ty_he expty
+ | NCic.Implicit `Vector::tl ->
+ let has_some_more_pis x =
+ match NCicReduction.whd ~subst context x with
+ | NCic.Meta _ | NCic.Appl (NCic.Meta _::_) -> false
+ | _ -> true
+ in
+ (try
+ aux metasenv subst args_so_far he ty_he tl
+ with
+ | Uncertain _
+ | RefineFailure _ as exc when has_some_more_pis ty_he ->
+ (try
+ aux metasenv subst args_so_far he ty_he
+ (NCic.Implicit `Term :: NCic.Implicit `Vector :: tl)
+ with
+ Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc)))