]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/paramodulation/utils.ml
new paramodulation
[helm.git] / helm / ocaml / paramodulation / utils.ml
index 681a371e1a6f71c60e90d7021aa1a8aa121c0688..2d5ee24ce7612527102a3f128c586fa66511145d 100644 (file)
@@ -289,9 +289,10 @@ let rec aux_ordering ?(recursion=true) t1 t2 =
       aux_ordering h1 h2
         
   | t1, t2 ->
-      debug_print (lazy (
-        Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n"
-          (CicPp.ppterm t1) (CicPp.ppterm t2)));
+      debug_print
+        (lazy
+           (Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n"
+              (CicPp.ppterm t1) (CicPp.ppterm t2)));
       Incomparable
 ;;