From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 19 Oct 2006 09:16:07 +0000 (+0000)
Subject: Bug fixed: when trying to insert coercions after an Uncertain, a RefineFailure
X-Git-Tag: make_still_working~6735
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=48dc3602a536a258db41a9923d560569567c9497;p=helm.git

Bug fixed: when trying to insert coercions after an Uncertain, a RefineFailure
was raised (instead of re-raising an Uncertain).
---

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 54055ebb6..0a6510b44 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1409,8 +1409,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                     (match coer with
                     | CoercGraph.NoCoercion 
                     | CoercGraph.NotHandled _ ->
-                        enrich localization_tbl hete
-                         (RefineFailure
+                        enrich localization_tbl hete exn
+                         ~f:(fun _ ->
                            (lazy ("The term " ^
                              CicMetaSubst.ppterm_in_context subst hete
                               context ^ " has type " ^
@@ -1419,8 +1419,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                              CicMetaSubst.ppterm_in_context subst s context
                               (* "\nReason: " ^ Lazy.force e*))))
                     | CoercGraph.NotMetaClosed -> 
-                        enrich localization_tbl hete
-                         (Uncertain
+                        enrich localization_tbl hete exn
+                         ~f:(fun _ ->
                            (lazy ("The term " ^
                              CicMetaSubst.ppterm_in_context subst hete
                               context ^ " has type " ^