From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 15 Feb 2009 14:57:16 +0000 (+0000)
Subject: commented some printings
X-Git-Tag: make_still_working~4200
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=abf25195eddebc8859736ff782cade507fdb780e;p=helm.git

commented some printings
---

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 7cdbf43d3..4745fecc2 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -1176,8 +1176,10 @@ let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
       prerr_endline (string_of_int (List.length expansionsl));
       prerr_endline (string_of_int (List.length expansionsr));
       *)
+(*
       if expansionsl <> [] then prerr_endline "expansionl";
       if expansionsr <> [] then prerr_endline "expansionr";
+*)
       List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
       @
       List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr