X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=614faf6df15f50d6af219ac90ccacf502afd04fb;hb=28ac70d3f475442cda4ef30e0e9c0e6d012b2527;hp=aea2a262526a20aaeea0caa6f4b2cdcb41d8c1f0;hpb=0319dd1bc1f0b431945f9641a587fa52d6472ebc;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index aea2a2625..614faf6df 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -47,7 +47,7 @@ let reset_counters () =
  metasenv_length := 0;
  context_length := 0
 let print_counters () =
-  debug_print (Printf.sprintf
+  debug_print (lazy (Printf.sprintf
 "apply_subst: %d
 apply_subst_context: %d
 apply_subst_metasenv: %d
@@ -64,7 +64,7 @@ context length: %d (avg = %.2f)
   ((float !metasenv_length) /. (float !apply_subst_metasenv_counter))
   !context_length
   ((float !context_length) /. (float !apply_subst_context_counter))
-  )*)
+  ))*)
 
 
 
@@ -573,10 +573,10 @@ let rec restrict subst to_be_restricted metasenv =
             (ppterm subst term)
 	  in 
           (* DEBUG
-          debug_print error_msg;
-          debug_print ("metasenv = \n" ^ (ppmetasenv metasenv subst));
-          debug_print ("subst = \n" ^ (ppsubst subst)); 
-          debug_print ("context = \n" ^ (ppcontext subst context)); *)
+          debug_print (lazy error_msg);
+          debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst)));
+          debug_print (lazy ("subst = \n" ^ (ppsubst subst)));
+          debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *)
           raise (MetaSubstFailure error_msg))) 
       subst ([], []) 
   in
@@ -592,8 +592,8 @@ let delift n subst context metasenv l t =
    otherwise the occur check does not make sense *)
 
 (*
- debug_print ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
- al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l)))); 
+ debug_print (lazy ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
+ al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l)))));
 *)
 
  let module S = CicSubstitution in
@@ -716,14 +716,14 @@ let delift n subst context metasenv l t =
       (* The reason is that our delift function is weaker than first  *)
       (* order (in the sense of alpha-conversion). See comment above  *)
       (* related to the delift function.                              *)
-(* debug_print "First Order UnificationFailure during delift" ;
-debug_print(sprintf
+(* debug_print (lazy "First Order UnificationFailure during delift") ;
+debug_print(lazy (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)
         (String.concat "; "
           (List.map
             (function Some t -> ppterm subst t | None -> "_") l
-          ))); *)
+          )))); *)
       raise (Uncertain (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)