Yet another refinement error localized.

Enrico should really learn to localize his own exceptions :-)

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 0ef14696c5d46c68075698cde0f36070629f072c..c2c3902e47df7432a4c224f48dcc0af2d2eff64a 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/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