From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 18 Sep 2008 11:13:39 +0000 (+0000)
Subject: In case of coercion to Prod, the error message shown is that _after_ the
X-Git-Tag: make_still_working~4773
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f386b970edc5798769c96e44f5c9ab30efa06605;p=helm.git

In case of coercion to Prod, the error message shown is that _after_ the
coercion. In case of multiple coercions, only one error is shown.
---

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 956372d60..f55b1fed0 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1308,6 +1308,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
                "\n but is applyed to: " ^ String.concat ";" 
                (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
+              let error = ref None in
               let possible_fixes = 
                fix_arity (List.length args) metasenv context subst he hetype
                 ugraph in
@@ -1325,14 +1326,18 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                    with
                     | RefineFailure _ | Uncertain _
                     | HExtlib.Localized (_,RefineFailure _)
-                    | HExtlib.Localized (_,Uncertain _) -> None)
+                    | HExtlib.Localized (_,Uncertain _) as exn ->
+                       error := Some exn; None)
                 possible_fixes
               with
               | Some x -> x
               | None ->
-                 raise 
-                  (MoreArgsThanExpected
-                    (List.length args, RefineFailure (lazy "")))
+                 match !error with
+                    None ->
+                     raise 
+                      (MoreArgsThanExpected
+                        (List.length args, RefineFailure (lazy "")))
+                  | Some exn -> raise exn
     in
     (* first we check if we are in the simple case of a meta closed term *)
     let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =