X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=62308896fd02b6b89bb420bd9c2c501c99273e54;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=fad86a854aeec9f7db327e70ba0dfec5cee78de8;hpb=e61d023695578ebf09d487480e6e7cac3a2dd2ee;p=helm.git

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index fad86a854..62308896f 100644
--- 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