fixed a couple of bugs that broke tests...

[helm.git] / helm / ocaml / paramodulation / indexing.ml

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 85ee885cb969755c55bb551b85ea88d6e6a09550..0e5914b11320de8a39d79ad5957ab09ecdee1ed5 100644 (file)
--- 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)))