X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=969d412cef43a28151e995250fdf10d2adc172c4;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=e92117334acb7cf22964be509ca75d7887ea671b;hpb=febd89f8a2b61f958e149ed630f5c991eb7d9661;p=helm.git

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index e92117334..969d412ce 100644
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -1055,7 +1055,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
 (*               let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
               let (head, newmetas, args, newmeta) =
                 ProofEngineHelpers.saturate_term newmeta []
-                  context (S.lift index term)
+                  context (S.lift index term) 0
               in
               let p =
                 if List.length args = 0 then
@@ -1161,7 +1161,7 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
           match termty with
           | C.Prod (name, s, t) ->
               let head, newmetas, args, newmeta =
-                ProofEngineHelpers.saturate_term newmeta [] context termty
+                ProofEngineHelpers.saturate_term newmeta [] context termty 0
               in
               let p =
                 if List.length args = 0 then