More debug_print made lazy.

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

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index a5221c22976f3d3c337121cbb116e82b7a0bb88c..b0bc8c623aaf5d1bdbc739b2f2090b9ca46af179 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -873,11 +873,11 @@ and type_of_aux' metasenv context t ugraph =
       try
        fo_unif_subst subst context metasenv hetype hetype' ugraph
       with exn ->
-       debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
+       debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
                         (CicPp.ppterm hetype)
                         (CicPp.ppterm hetype')
                          (CicMetaSubst.ppmetasenv [] metasenv)
-                        (CicMetaSubst.ppsubst subst));
+                        (CicMetaSubst.ppsubst subst)));
        raise exn
 
     in
@@ -1070,16 +1070,16 @@ let type_of_aux' metasenv context term =
  try
   let (t,ty,m) = 
       type_of_aux' metasenv context term in
-    debug_print
-     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
-   debug_print
-    ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
+    debug_print (lazy
+     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
+   debug_print (lazy
+    ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
    (t,ty,m)
  with
  | RefineFailure msg as e ->
-     debug_print ("@@@ REFINE FAILED: " ^ msg);
+     debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
      raise e
  | Uncertain msg as e ->
-     debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
+     debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
      raise e
 ;; *)