subst,metasenv,ugraph,hetype,he,args_bo_and_ty
else
(* this (says CSC) is also useful to infer dependent types *)
- fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
+ try
+ fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
+ with RefineFailure _ | Uncertain _ as exn ->
+ (* unable to fix arity *)
+ more_args_than_expected localization_tbl
+ subst he context hetype args_bo_and_ty exn
in
let coerced_args,subst,metasenv,he,t,ugraph =
eat_prods_and_args