captured exception preserved (was replaced blindly with a RefineFailure)

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index a73313ebae5f6047de9f40d464493a39336b18fc..2ef492bc8e99aa436ba9b74efafcaf85c34acf0b 100644 (file)
--- 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