From 43c2a5068c1ff5f838e0558bb60c21e316cab852 Mon Sep 17 00:00:00 2001
From: Alberto Griggio <griggio@fbk.eu>
Date: Wed, 12 Oct 2005 12:37:36 +0000
Subject: [PATCH] fixed a couple of bugs that broke tests...

---
 helm/ocaml/paramodulation/indexing.ml   | 10 ----------
 helm/ocaml/paramodulation/inference.ml  |  6 ++++--
 helm/ocaml/paramodulation/saturation.ml | 10 +++++-----
 3 files changed, 9 insertions(+), 17 deletions(-)

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 85ee885cb..0e5914b11 100644
--- 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)))
diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index bf53f5cec..e4451769a 100644
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -1184,8 +1184,10 @@ let find_library_equalities dbd context status maxmeta =
     | C.Meta _ | C.Rel _ | C.Const _ -> false
     | C.Var _ -> true
     | C.Appl l -> List.exists has_vars l
-    | C.Prod (_, s, t) -> (has_vars s) || (has_vars t)
-    | _ -> assert false
+    | C.Prod (_, s, t) | C.Lambda (_, s, t)
+    | C.LetIn (_, s, t) | C.Cast (s, t) ->
+        (has_vars s) || (has_vars t)
+    | _ -> false
   in
   let rec aux newmeta = function
     | [] -> [], newmeta
diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 181b4e1d9..00e266ce3 100644
--- 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 ->
-- 
2.39.2