From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 20 May 2006 10:08:43 +0000 (+0000)
Subject: removed prerr_endline
X-Git-Tag: make_still_working~7348
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b6f33efbe92819ac15ce05b8cd9e66d3db50abcb;p=helm.git

removed prerr_endline
---

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 6ab9f59e2..8a31d6253 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1800,7 +1800,6 @@ let saturate
       let goal_proof = replace goal_proof in
         (* ok per le meta libere... ma per quelle che c'erano e sono rimaste? 
          * what mi pare buono, sostituisce solo le meta farlocche *)
-        prerr_endline (CicPp.pp goal_proof names);
       let side_effects_t = List.map replace side_effects_t in
       (* check/refine/... build the new proof *)
       let replaced_goal =