try
Cic.CicHash.find localization_tbl t
with Not_found ->
- prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
+ HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
raise exn'
in
raise (HExtlib.Localized (loc,exn'))
enrich localization_tbl he ~f:(fun _-> msg) exn
;;
-let mk_prod_of_metas metasenv context' subst args =
+let mk_prod_of_metas metasenv context subst args =
let rec mk_prod metasenv context' = function
| [] ->
let (metasenv, idx) =
(* then I generate a name --- using the hint name_hint *)
(* --- that is fresh in context'. *)
let name_hint =
- (* Cic.Name "pippo" *)
FreshNamesGenerator.mk_fresh_name ~subst metasenv
- (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
- (CicMetaSubst.apply_subst_context subst context')
+ (CicMetaSubst.apply_subst_context subst context)
Cic.Anonymous
~typ:(CicMetaSubst.apply_subst subst argty)
in
- (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
FreshNamesGenerator.mk_fresh_name ~subst
[] context' name_hint ~typ:(Cic.Sort Cic.Prop)
in
in
metasenv,Cic.Prod (name,meta,target)
in
- mk_prod metasenv context' args
+ mk_prod metasenv context args
;;
let rec type_of_constant uri ugraph =
exn ->
enrich localization_tbl term' exn
~f:(function _ ->
- lazy ("(10)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst term'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
exn ->
enrich localization_tbl constructor'
~f:(fun _ ->
- lazy ("(11)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context metasenv subst p'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context metasenv subst actual_type
exn ->
enrich localization_tbl p exn
~f:(function _ ->
- lazy ("(12)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst p
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst instance'
exn ->
enrich localization_tbl bo exn
~f:(function _ ->
- lazy ("(13)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
exn ->
enrich localization_tbl bo exn
~f:(function _ ->
- lazy ("(14)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
(* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
" <==> " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst t context));
+ CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
+ "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
+ context));
debug_print (lazy ("FO_UNIF_SUBST: " ^
CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
let subst,metasenv,ugraph =
fo_unif_subst subst context metasenv infty expty ugraph
in
(t, expty), subst, metasenv, ugraph
- with Uncertain _ | RefineFailure _ as exn ->
- if not allow_coercions || not !insert_coercions then
- enrich localization_tbl t exn
- else
+ with (Uncertain _ | RefineFailure _ as exn)
+ when allow_coercions && !insert_coercions ->
let whd = CicReduction.whd ~delta:false in
let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
let infty = clean infty subst context in