1. PrimitiveTactics.new_metasenv_for_apply changed a little bit, moved to

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

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index fad86a854aeec9f7db327e70ba0dfec5cee78de8..62308896fd02b6b89bb420bd9c2c501c99273e54 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -996,18 +996,10 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
           match term with
           | C.Prod (name, s, t) ->
 (*               let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
-              let (head, newmetas, args, _) =
-                PrimitiveTactics.new_metasenv_for_apply newmeta proof
+              let (head, newmetas, args, newmeta) =
+                ProofEngineHelpers.saturate_term newmeta []
                   context (S.lift index term)
               in
-              let newmeta =
-                List.fold_left
-                  (fun maxm arg ->
-                     match arg with
-                     | C.Meta (i, _) -> (max maxm i)
-                     | _ -> assert false)
-                  newmeta args
-              in
               let p =
                 if List.length args = 0 then
                   C.Rel index