fixed bugs in Indexing.find_matches and Saturation.apply_equality_to_goal

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

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 0556c442df8146f7c6f50961dc44149f400d4a18..bf53f5cec8acc8823b0906a9fe2c558011818c12 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -1180,6 +1180,13 @@ let find_library_equalities dbd context status maxmeta =
   let ok_types ty menv =
     List.for_all (fun (_, _, mt) -> mt = ty) menv
   in
+  let rec has_vars = function
+    | 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
+  in
   let rec aux newmeta = function
     | [] -> [], newmeta
     | (uri, term, termty)::tl ->
@@ -1189,7 +1196,7 @@ let find_library_equalities dbd context status maxmeta =
                 (CicPp.ppterm term) (CicPp.ppterm termty)));
         let res, newmeta = 
           match termty with
-          | C.Prod (name, s, t) ->
+          | C.Prod (name, s, t) when not (has_vars termty) ->
               let head, newmetas, args, newmeta =
                 ProofEngineHelpers.saturate_term newmeta [] context termty 0
               in
@@ -1212,7 +1219,8 @@ let find_library_equalities dbd context status maxmeta =
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
-          | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
+          | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+              when iseq uri && not (has_vars termty) ->
               let o = !Utils.compare_terms t1 t2 in
               let w = compute_equality_weight ty t1 t2 in
               let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in