new version of auto that is able to prove the irrationality of sqrt(2)

[helm.git] / helm / software / components / tactics / paramodulation / test_indexing.ml

diff --git a/helm/software/components/tactics/paramodulation/test_indexing.ml b/helm/software/components/tactics/paramodulation/test_indexing.ml
index ba6b2ebe062c173735685f50a30f7dab27a2a87c..02dbf69e0b4ccc88b4ed25e171dfc685538bbe38 100644 (file)
--- 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);
 ;;