X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=c2c3902e47df7432a4c224f48dcc0af2d2eff64a;hb=914ebf94df588f5a1eef9ba62900259e9570f6b3;hp=bd8e992d0bfdef7d8b3eddc39a0a4b4c1a25ed90;hpb=cb4b3b6d71a8d0b5120fe6604cc55105637ef234;p=helm.git

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index bd8e992d0..c2c3902e4 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -34,8 +34,8 @@ exception AssertFailure of string Lazy.t;;
 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"
 
@@ -1492,7 +1492,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
       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