From: Claudio Sacerdoti Coen Date: Thu, 22 Mar 2007 16:20:36 +0000 (+0000) Subject: Debugging code removed. X-Git-Tag: make_still_working~6420 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=38d3574438b4f764ad433915c9733cc73a684b39;p=helm.git Debugging code removed. --- diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 6e963a274..576721be3 100644 --- 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 5afc67269..685baff9b 100644 --- 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