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'))
| Some t,Some (_,C.Def (ct,_)) ->
let subst',metasenv',ugraph' =
(try
-prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");
+(*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
+ * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
fo_unif_subst subst context metasenv t ct ugraph
with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
in
(* {{{ *) 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 =