Debugging code removed.

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 6e963a274d06befaf6e6e897009e88aad9a9473c..576721be3542c1b67a098c05f0fbbadede1e2f85 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -1121,7 +1121,6 @@ let normalize ?delta ?subst ctx term =
   
 (* performs an head beta/cast reduction *)
 let rec head_beta_reduce ?(delta=false) ?(upto=(-1)) t =
- HLog.warn (Printf.sprintf "inside head_beta_reduce %i %s" upto (CicPp.ppterm t));
  match upto with
     0 -> t
   | n ->

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