X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=359b5b0761c12691d91ce5725a84516fefcdd664;hb=0e81e658803822599b5e015aab67bc282afc9c4d;hp=020b819c93ac8df0a5388e7de764bc75a6053b2c;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 020b819c9..359b5b076 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -1510,10 +1510,12 @@ let rec auto_clusters ?(top=false)
     let classes = HExtlib.clusters (deps status) all_goals in
     List.iter 
 	(fun gl ->
-	   if List.length gl > flags.maxwidth then 
-	     (debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); 
-	      raise (Gaveup IntSet.empty))
-	   else ()) classes;
+	   if List.length gl > flags.maxwidth then begin
+	      debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); 
+	      HLog.error (sprintf "global width (%u) exceeded: %u"
+	         flags.maxwidth (List.length gl));
+	      raise (Gaveup IntSet.empty)
+	   end else ()) classes;
     if List.length classes = 1 then
       let flags = 
         {flags with last = (List.length all_goals = 1)} in 
@@ -1595,9 +1597,12 @@ auto_main flags signature cache depth status: unit =
 	else
         let ng = List.length goals in
         (* moved inside auto_clusters *)
-        if ng > flags.maxwidth then 
-          (print ~depth (lazy "FAIL LOCAL WIDTH"); raise (Gaveup IntSet.empty))
-        else if depth = flags.maxdepth then 
+        if ng > flags.maxwidth then begin 
+          debug_print ~depth (lazy "FAIL LOCAL WIDTH");
+	  HLog.error (sprintf "local width (%u) exceeded: %u"
+	     flags.maxwidth ng);
+	  raise (Gaveup IntSet.empty)
+        end else if depth = flags.maxdepth then
 	  raise (Gaveup IntSet.empty)
         else 
         let status = NTactics.branch_tac ~force:true status in
@@ -1710,7 +1715,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
   app_counter:= 0;
   let rec up_to x y =
     if x > y then
-      (print(lazy
+      (debug_print(lazy
         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
        debug_print(lazy
         ("Applicative nodes:"^string_of_int !app_counter));