(* 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 =
" but is here used with type " ^
CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
in
- match exn with
- RefineFailure _ -> raise (HExtlib.Localized (loc,RefineFailure msg))
- | Uncertain _ -> raise (HExtlib.Localized (loc,Uncertain msg))
- | _ -> assert false
+ let exn' =
+ match exn with
+ RefineFailure _ -> RefineFailure msg
+ | Uncertain _ -> Uncertain msg
+ | _ -> assert false
+ in
+ raise (HExtlib.Localized (loc exn',exn'))
in
let bo' = CicMetaSubst.apply_subst subst bo' in
let ty' = CicMetaSubst.apply_subst subst ty' in