- | []->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
+ (match NCicReduction.whd ~subst context ty_he with
+ NCic.Meta _ | NCic.Appl (NCic.Meta _::_) ->
+ too_many_args := true;
+ | _ -> ());
+ force_ty true false metasenv subst context orig_t res ty_he expty
+ | NCic.Implicit `Vector::tl ->
+ (try
+ too_many_args := false;
+ aux metasenv subst args_so_far he ty_he tl
+ with
+ Uncertain _
+ | RefineFailure _ as exc when !too_many_args <> true ->
+ try
+ aux metasenv subst args_so_far he ty_he
+ (NCic.Implicit `Vector :: NCic.Implicit `Term :: tl)
+ with
+ Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc))