removed ugly prerr_endline

[helm.git] / components / cic_unification / cicRefine.ml

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index e0f8fd1c79128ad1663640690a167c931ce623cb..e4f4ef8e0c002a600f791d37ec2f9524730dbefb 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -91,7 +91,7 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn =
   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'))
@@ -1334,7 +1334,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 (* {{{ *) 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 =