From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 15 Sep 2006 21:35:36 +0000 (+0000)
Subject: Yet another refinement error localized.
X-Git-Tag: make_still_working~6885
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cb4df34c6cc22be1fe992c1dc4242122b3fa6979;p=helm.git

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 0ef14696c..c2c3902e4 100644
--- 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