From f386b970edc5798769c96e44f5c9ab30efa06605 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 18 Sep 2008 11:13:39 +0000 Subject: [PATCH] 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. --- .../components/cic_unification/cicRefine.ml | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) 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 = -- 2.39.2