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

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 0ef14696c..c2c3902e4 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -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