From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 19 Feb 2010 07:36:11 +0000 (+0000)
Subject: Nuova versione di auto.
X-Git-Tag: make_still_working~3036
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f6fdc9a280341b52ba0ec7a770e1abd552e6b704;p=helm.git

Nuova versione di auto.
---

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index f64bb20ac..ec92ff135 100644
--- 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 =