Debugging code removed.

[helm.git] / helm / software / components / cic_proof_checking / cicReduction.ml

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 ->