fixed a couple of bugs that broke tests...

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 85ee885cb969755c55bb551b85ea88d6e6a09550..0e5914b11320de8a39d79ad5957ab09ecdee1ed5 100644 (file)
--- 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 bf53f5cec8acc8823b0906a9fe2c558011818c12..e4451769a53df3ee01ba626758d0e88ecbcc4533 100644 (file)
--- 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 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 ->