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 54055ebb6478633c47f3e2f952b6f1c11a707c93..0a6510b445ad1957681f60db8faf51b7ba18072d 100644 (file)
--- 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 " ^