fixed a couple of bugs that broke tests...

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

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