Build_proof_goal does not return the metasenv any more.

[helm.git] / components / tactics / paramodulation / saturation.ml

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index d5da5485f72526bc4ded022d3953dc7acd5ff50e..4423661b00b118073a45e4d0d071bfec56c8921a 100644 (file)
--- 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