X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Ftest_indexing.ml;h=02dbf69e0b4ccc88b4ed25e171dfc685538bbe38;hb=3a0c71609f757f4ad3aadd234b84486fec97b791;hp=ba6b2ebe062c173735685f50a30f7dab27a2a87c;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/test_indexing.ml b/helm/software/components/tactics/paramodulation/test_indexing.ml
index ba6b2ebe0..02dbf69e0 100644
--- a/helm/software/components/tactics/paramodulation/test_indexing.ml
+++ b/helm/software/components/tactics/paramodulation/test_indexing.ml
@@ -72,7 +72,7 @@ let differing () =
   in
   let res = Inference.extract_differing_subterms t1 t2 in
   match res with
-  | None -> print_endline "NO DIFFERING SUBTERMS???"
+  | None -> prerr_endline "NO DIFFERING SUBTERMS???"
   | Some (t1, t2) ->
       Printf.printf "OK: %s, %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2);
 ;;