Nuova versione di auto.

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index f64bb20acef98da8b2a81d5cd07c0a4485050021..ec92ff1353e7b48816c005c50d6b2f64eadad73d 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -1477,7 +1477,7 @@ let height_of_goals status =
             ) 
         context)
      open_goals;
-  prerr_endline ("altezza sequente: " ^ string_of_int !h);
+  debug_print ("altezza sequente: " ^ string_of_int !h);
   !h
 ;;
 
@@ -1646,7 +1646,7 @@ exception Found
 (* gty is supposed to be meta-closed *)
 let is_subsumed depth status gty cache =
   if cache=[] then false else (
-  print ~depth (lazy("Subsuming " ^ (ppterm status gty))); 
+  debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty))); 
   let n,h,metasenv,subst,obj = status#obj in
   let ctx = ctx_of gty in
   let _ , target = term_of_cic_term status gty ctx in
@@ -1974,7 +1974,7 @@ auto_main flags signature (cache:cache) depth status: unit =
         let status, gty = apply_subst status gctx gty in
         debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty)); 
         if is_subsumed depth status closegty (snd cache.under_inspection) then 
-          (print ~depth (lazy "SUBSUMED");
+          (debug_print ~depth (lazy "SUBSUMED");
            raise (Gaveup IntSet.add g IntSet.empty))
         else 
         let do_flags =