From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 30 Aug 2007 16:47:15 +0000 (+0000)
Subject: captured exception preserved (was replaced blindly with a RefineFailure)
X-Git-Tag: 0.4.95@7852~234
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=40d489654171aeb8e96c6d5dcd3d8976705e8517;p=helm.git

captured exception preserved (was replaced blindly with a RefineFailure)
---

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index a73313eba..2ef492bc8 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/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