fixed a couple of bugs that broke tests...

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

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 181b4e1d9a39da08039858250d290025925d1ca6..00e266ce33fcd06fc17567ceb4d8eca526749f9c 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -942,10 +942,10 @@ let apply_equality_to_goal env equality goal =
   let eqterm =
     C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in
   let gproof, gmetas, gterm = goal in
-  debug_print
-    (lazy
-       (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s"
-          (string_of_equality equality) (CicPp.ppterm gterm)));
+(*   debug_print *)
+(*     (lazy *)
+(*        (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s" *)
+(*           (string_of_equality equality) (CicPp.ppterm gterm))); *)
   try
     let subst, metasenv', _ =
       let menv = metasenv @ metas @ gmetas in
@@ -1177,7 +1177,7 @@ let apply_to_goal env theorems ?passive active goal =
   in
   let r, s, l =
     if Inference.term_is_equality term then
-      let _ = debug_print (lazy "OK, is equality!!") in
+(*       let _ = debug_print (lazy "OK, is equality!!") in *)
       let rec appleq_a = function
         | [] -> false, [], []
         | (Positive, equality)::tl ->