X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;fp=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=0e5914b11320de8a39d79ad5957ab09ecdee1ed5;hb=43c2a5068c1ff5f838e0558bb60c21e316cab852;hp=85ee885cb969755c55bb551b85ea88d6e6a09550;hpb=71c9c97dfca2393bd6d90ea45f6d2e4e6ae15793;p=helm.git

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 85ee885cb..0e5914b11 100644
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -998,16 +998,6 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
 (*     | _, _, (_, left, right, _), _, _ -> *)
 (*         not (fst (CR.are_convertible context left right ugraph)) *)
 (*   in *)
-  let _ =
-    let env = metasenv, context, ugraph in
-    debug_print
-      (lazy
-         (Printf.sprintf "end of superposition_right:\n%s\n"
-            (String.concat "\n"
-               ((List.map
-                   (fun e -> "Positive " ^
-                      (Inference.string_of_equality ~env e)) (new1 @ new2))))))
-  in
   let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
   (!maxmeta,
    (List.filter ok (new1 @ new2)))