X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=cb12f7a77c6ffbc335de5c4cf7f680dab55f5fea;hb=25564c06c570e5ab9be455904c0b381842f8d4c4;hp=5888019e4f78f584c047478a3a13d22b8177561e;hpb=91f0c0e84bfe6bf22e960d466e16f7260a2882ee;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 5888019e4..cb12f7a77 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -1365,7 +1365,8 @@ let draw_proof bag names goal_proof proof id =
   ignore(Unix.system "gv /tmp/matita_paramod.eps");
 ;;
 
-let saturate_term (id_to_eq, maxmeta) metasenv context term = 
+let saturate_term (id_to_eq, maxmeta) metasenv subst context term = 
+  let maxmeta = max maxmeta (CicMkImplicit.new_meta metasenv subst) in
   let head, metasenv, args, newmeta =
     TermUtil.saturate_term maxmeta metasenv context term 0
   in