From 14139694d817bd900f7f0fb412c69cf431baaad9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 4 Dec 2007 17:51:09 +0000 Subject: [PATCH] Some terms are not localized from the very beginning :-( --- helm/software/components/cic_unification/cicRefine.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 9099c262f..970d3e05f 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1832,10 +1832,12 @@ let typecheck metasenv uri obj ~localization_tbl = (* CSC: ugly code. Here I need to retrieve in advance the loc of bo since type_of_aux' destroys localization information (which are preserved by type_of_aux *) - let loc = + let loc exn' = try Cic.CicHash.find localization_tbl bo - with Not_found -> assert false in + with Not_found -> + HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo); + raise exn' in let bo',boty,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv [] bo ugraph in let ty',_,metasenv,ugraph = @@ -1855,8 +1857,8 @@ let typecheck metasenv uri obj ~localization_tbl = CicMetaSubst.ppterm_in_context ~metasenv [] ty' []) in match exn with - RefineFailure _ -> raise (HExtlib.Localized (loc,RefineFailure msg)) - | Uncertain _ -> raise (HExtlib.Localized (loc,Uncertain msg)) + RefineFailure _ -> raise (HExtlib.Localized (loc exn,RefineFailure msg)) + | Uncertain _ -> raise (HExtlib.Localized (loc exn,Uncertain msg)) | _ -> assert false in let bo' = CicMetaSubst.apply_subst subst bo' in -- 2.39.2