]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_unification/cicUnification.ml
More debug_print made lazy.
[helm.git] / helm / ocaml / cic_unification / cicUnification.ml
index fe5ae76502ba2703cbb70519186eb1d29872abfb..27150461fb0038ba4c5e7d81f8ff0562d0dc2de3 100644 (file)
@@ -291,7 +291,7 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
                             with
                                 Uncertain _
                               | UnificationFailure _ ->
-debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)); 
+debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j))); 
                                   let metasenv, subst = 
                                     CicMetaSubst.restrict 
                                       subst [(n,j)] metasenv in
@@ -346,7 +346,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin
                 UnificationFailure msg ->raise (UnificationFailure msg)  
               | Uncertain msg -> raise (UnificationFailure (Reason msg))
               | AssertFailure _ ->
-                  debug_print "siamo allo huge hack";
+                  debug_print (lazy "siamo allo huge hack");
                   (* TODO huge hack!!!!
                    * we keep on unifying/refining in the hope that 
                    * the problem will be eventually solved.