More debug_print made lazy.

[helm.git] / helm / ocaml / cic_unification / coercGraph.ml

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index 57274e616446b3dab7b416c8db8f71f3aace8441..c6a929619f508d65bbeb6c307093322422683b54 100644 (file)
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -26,7 +26,7 @@
 open Printf;;
 
 let debug = false
-let debug_print = if debug then prerr_endline else ignore
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (* searches a coercion fron src to tgt in the !coercions list *)
 let look_for_coercion src tgt =
@@ -38,17 +38,17 @@ let look_for_coercion src tgt =
           (fun (s,t) -> UriManager.eq s src && UriManager.eq t tgt) 
       in
       match l with
-      | [] -> debug_print ":( coercion non trovata"; None
+      | [] -> debug_print (lazy ":( coercion non trovata"); None
       | u::_ -> 
-          debug_print (
+          debug_print (lazy (
             sprintf ":) TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" 
               (List.length l)
               (UriManager.name_of_uri src) 
               (UriManager.name_of_uri tgt)
-              (UriManager.name_of_uri u));
+              (UriManager.name_of_uri u)));
               Some (CicUtil.term_of_uri u)
     with Invalid_argument s -> 
-      debug_print (":( coercion non trovata (fallita la uri_of_term): " ^ s);
+      debug_print (lazy (":( coercion non trovata (fallita la uri_of_term): " ^ s));
       None
 ;;
 
@@ -97,8 +97,8 @@ let generate_composite_closure c1 c2 univ =
     try 
       CicTypeChecker.type_of_aux' [] [] c univ
     with CicTypeChecker.TypeCheckerFailure s as exn ->
-      debug_print (sprintf "Generated composite coercion:\n%s\n%s" 
-        (CicPp.ppterm c) s);
+      debug_print (lazy (sprintf "Generated composite coercion:\n%s\n%s" 
+        (CicPp.ppterm c) s));
       raise exn
   in
   let cleaned_ty =