X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=4423661b00b118073a45e4d0d071bfec56c8921a;hb=d5950e1810f3a6d89328f18c2c5796e54a907473;hp=d5da5485f72526bc4ded022d3953dc7acd5ff50e;hpb=1f82709017e4ec5bab8e0311e00992b89572d856;p=helm.git

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index d5da5485f..4423661b0 100644
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -857,7 +857,7 @@ let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table =
                    repl proof
                in
                let newcicp,np,subst,cicmenv = 
-                 cicproof,np, subst, (m @ menv) 
+                 cicproof,np, subst, Equality.apply_subst_metasenv subst (m @ menv) 
                in
                  Some 
                   ((newcicp,np,subst,cicmenv),
@@ -1492,14 +1492,10 @@ let saturate
       let cic_proof = Equality.build_proof_term_old proof in
      
       (* generation of the new proof *)
-      let cic_proof_new,cic_proof_new_menv = 
+      let cic_proof_new = 
         Equality.build_goal_proof 
           goalproof (Equality.build_proof_term_new newproof) 
       in
-      let newproof_menv = 
-        Equality.apply_subst_metasenv subsumption_subst 
-          (newproof_menv @ cic_proof_new_menv)
-      in
       let cic_proof_new = 
         Equality.apply_subst subsumption_subst cic_proof_new 
       in