From 38d3574438b4f764ad433915c9733cc73a684b39 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 22 Mar 2007 16:20:36 +0000 Subject: [PATCH] Debugging code removed. --- helm/software/components/cic_proof_checking/cicReduction.ml | 1 - helm/software/components/tactics/reductionTactics.ml | 5 ----- 2 files changed, 6 deletions(-) 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 -- 2.39.2