X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=4745fecc2e5a971bfe53d90510422c4a164d227d;hb=79a489c46c77de80979d68a512d1f640f8273f9e;hp=7cdbf43d38a2242938c5f83c710f08f3cfe08761;hpb=d990d5c64d0b9c07baef4257e7931321a42ae695;p=helm.git

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