From 4fb01ad004146d7563e14dc4901731eb8010f640 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 28 Nov 2005 13:25:04 +0000 Subject: [PATCH] More aggressive politic for non localized terms: an assert false! --- helm/ocaml/cic_unification/cicRefine.ml | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 661d5c34c..18ed5a076 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -43,16 +43,20 @@ in profiler.HExtlib.profile foo () | (CicUnification.Uncertain msg) -> raise (Uncertain msg) ;; -let enrich loc f exn = +let enrich localization_tbl t f exn = let exn' = match exn with RefineFailure msg -> RefineFailure (f msg) | Uncertain msg -> Uncertain (f msg) - | _ -> assert false + | _ -> assert false in + let loc = + try + Cic.CicHash.find localization_tbl t + with Not_found -> + (* prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); *) + assert false in - match loc with - None -> raise exn' - | Some loc -> raise (HExtlib.Localized (loc,exn')) + raise (HExtlib.Localized (loc,exn')) let relocalize localization_tbl oldt newt = try @@ -1023,9 +1027,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t CicMetaSubst.ppterm_in_context subst s context (* "\nReason: " ^ Lazy.force e*)) in - enrich - (try Some (Cic.CicHash.find localization_tbl hete) with Not_found -> prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm hete); None) - msg exn + enrich localization_tbl hete msg exn | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy "Coercions on meta")) | CoercGraph.SomeCoercion c -> -- 2.39.2