From dc151c78b57bae7de8ec8417925ade6c0d7b1db0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 15 Nov 2007 13:33:53 +0000 Subject: [PATCH] removed ugly prerr_endline --- helm/software/components/cic_unification/cicRefine.ml | 2 +- helm/software/components/tactics/auto.ml | 8 ++++---- helm/software/configure.ac | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index f680b01f1..e4f4ef8e0 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -91,7 +91,7 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn = try Cic.CicHash.find localization_tbl t with Not_found -> - prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); + HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); raise exn' in raise (HExtlib.Localized (loc,exn')) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index a7af3bbe5..b9ce25174 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -1249,7 +1249,7 @@ let prunable menv subst ty todo = | (D (_,_,T))::tl -> aux tl | _ -> false and no_progress variant = function - | [] -> prerr_endline "++++++++++++++++++++++++ no_progress"; true + | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true | D ((n,_,P) as g)::tl -> (match calculate_goal_ty g subst menv with | None -> no_progress variant tl @@ -1345,7 +1345,7 @@ let auto_main tables maxm context flags universe cache elems = (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize)); aux tables maxm flags cache orlist) else if prunable_for_size flags s m todo then - (prerr_endline ("POTO at depth: "^(string_of_int depth)); + (debug_print (lazy ("POTO at depth: "^(string_of_int depth))); aux tables maxm flags cache orlist) else (* still to be proved *) @@ -1716,8 +1716,8 @@ let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) = in match auto_main tables newmeta context flags universe cache [elem] with | Proved (metasenv,subst,_, tables,cache,_) -> - prerr_endline - ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)); + (*prerr_endline + ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));*) let proof,metasenv = ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof goal subst metasenv diff --git a/helm/software/configure.ac b/helm/software/configure.ac index 90e1dc286..8ca52e37c 100644 --- a/helm/software/configure.ac +++ b/helm/software/configure.ac @@ -5,7 +5,7 @@ AC_INIT(matita/matitaTypes.ml) DEBUG_DEFAULT="true" DEFAULT_DBHOST="mysql://mowgli.cs.unibo.it" RT_BASE_DIR_DEFAULT="`pwd`/matita" -MATITA_VERSION="0.4.95" +MATITA_VERSION="0.4.96" DISTRIBUTED="no" # "yes" for distributed tarballs # End of distribution settings -- 2.39.2