From 803959f90ae806a62746efe7f557ecd4b70c16ee Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 9 Jan 2006 12:54:59 +0000 Subject: [PATCH] removed debugging printing --- helm/ocaml/paramodulation/inference.ml | 4 +--- helm/ocaml/paramodulation/utils.ml | 4 ++-- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 5a2fd042d..04cdb0aeb 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -919,12 +919,10 @@ type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;; let is_identity ((metasenv, context, ugraph) as env) = function | ((_, _, (ty, left, right, _), menv, _) as equality) -> - (prerr_endline ("left = "^(CicPp.ppterm left)); - prerr_endline ("right = "^(CicPp.ppterm right)); (left = right || (* (meta_convertibility left right) || *) (fst (CicReduction.are_convertible - ~metasenv:(metasenv @ menv) context left right ugraph)))) + ~metasenv:(metasenv @ menv) context left right ugraph))) ;; diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index 26d97b72a..5eb591c0b 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -566,8 +566,8 @@ let guarded_simpl context t = let t' = ProofEngineReduction.simpl context t in let simpl_order = !compare_terms t t' in if simpl_order = Gt then - (prerr_endline ("reduce: "^(CicPp.ppterm t)^(CicPp.ppterm t')); - t') + (* prerr_endline ("reduce: "^(CicPp.ppterm t)^(CicPp.ppterm t')); *) + t' else t ;; -- 2.39.2