Debugging code removed.

[helm.git] / helm / software / components / tactics / reductionTactics.ml

diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml
index 5afc672695733cada18b7335705e1d360bec515b..685baff9be8ecea7dfb4885ad9965bd8b7aa8199 100644 (file)
--- a/helm/software/components/tactics/reductionTactics.ml
+++ b/helm/software/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