From 54f0b41903d53877ac385506aa6d943cc4e40ade Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 19 Oct 2006 09:16:07 +0000 Subject: [PATCH] Bug fixed: when trying to insert coercions after an Uncertain, a RefineFailure was raised (instead of re-raising an Uncertain). --- components/cic_unification/cicRefine.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 54055ebb6..0a6510b44 100644 --- a/components/cic_unification/cicRefine.ml +++ b/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 " ^ -- 2.39.2