let insert_coercions = ref true
let pack_coercions = ref true
-(* let debug_print = fun _ -> () *)
- let debug_print x = prerr_endline (Lazy.force x);;
+let debug_print = fun _ -> ();;
+(*let debug_print x = prerr_endline (Lazy.force x);;*)
let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
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