X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FreductionTactics.ml;h=685baff9be8ecea7dfb4885ad9965bd8b7aa8199;hb=7c84225a8e472e754f1baf8f8b37f8627c8da6fa;hp=5afc672695733cada18b7335705e1d360bec515b;hpb=2a39b3fe15889f379932c642f4775a5f8e756022;p=helm.git

diff --git a/components/tactics/reductionTactics.ml b/components/tactics/reductionTactics.ml
index 5afc67269..685baff9b 100644
--- a/components/tactics/reductionTactics.ml
+++ b/components/tactics/reductionTactics.ml
@@ -119,11 +119,6 @@ let normalize_tac ~pattern =
   ~reduction:(const_lazy_reduction CicReduction.normalize) ~pattern)
 
 let head_beta_reduce_tac ?delta ?upto ~pattern =
- begin match upto with
-    | Some upto -> 
-         HLog.warn (Printf.sprintf "inside head_beta_reduce_tac %i" upto)
-    | None -> HLog.warn (Printf.sprintf "inside head_beta_reduce_tac none")
- end;
  mk_tactic (reduction_tac
   ~reduction:
     (const_lazy_reduction