From: Andrea Asperti 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 =