removed debug prerr_endline

[helm.git] / helm / ocaml / tactics / tacticals.ml

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 0479264d45d5a82b165f6cdbb896d5c56b4b5374..4e0e04914bd1ac9bcafa04f8c9d1c1c4cff14308 100644 (file)
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -31,11 +31,12 @@ open UriManager
 
   (** perform debugging output? *)
 let debug = false
+let debug_print = fun _ -> ()
 
   (** debugging print *)
 let warn s =
   if debug then
-    prerr_endline ("TACTICALS WARNING: " ^ s)
+    debug_print ("TACTICALS WARNING: " ^ s)
 
 
 (** TACTIC{,AL}S *)
@@ -255,10 +256,10 @@ let prova_tac =
       | (Some (Cic.Name name,_))::_ when name = "T" -> n
       | _::tl -> find (n+1) tl
     in
-     prerr_endline ("eseguo find");
+     debug_print ("eseguo find");
      find 1 context
    in
-    prerr_endline ("eseguo apply");    
+    debug_print ("eseguo apply");    
     apply_tac ~term:(Cic.Rel rel) status
  in
 (*  do_tactic ~n:2 *)