From ced1cde9425472e3bd032756e7bb3ef031c7f08d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 30 Aug 2007 16:47:15 +0000 Subject: [PATCH] captured exception preserved (was replaced blindly with a RefineFailure) --- helm/software/components/cic_unification/cicRefine.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index a73313eba..2ef492bc8 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1445,15 +1445,15 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il in try coerce_to_something_aux t infty expty subst metasenv context ugraph - with Uncertain _ | RefineFailure _ -> - let exn = - RefineFailure (lazy ("The term " ^ + with Uncertain _ | RefineFailure _ as exn -> + let f _ = + lazy ("The term " ^ CicMetaSubst.ppterm_in_context metasenv subst t context ^ " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst infty context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context metasenv subst expty context)) + CicMetaSubst.ppterm_in_context metasenv subst expty context) in - enrich localization_tbl t exn + enrich localization_tbl ~f t exn and coerce_to_sort localization_tbl t infty subst context metasenv uragph = match CicReduction.whd ~subst:subst context infty with -- 2.39.2