X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=f8b0ff45fcc088dcc5c799c93e8831c9be2f3b2b;hb=e1f0bb910f75b8b21f2c5e394ebb4c5a63ef4945;hp=f8b12c11952051f3736ab24d314b6bc74aed15fd;hpb=4e0ce221e8f218bbf60885173d61ea6ff9324213;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index f8b12c119..f8b0ff45f 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1319,7 +1319,7 @@ let build_proof
   if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA"
   else prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
   let proof, goalno = status in
-  let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
+  let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
   let names = Utils.names_of_context context in
@@ -1394,7 +1394,7 @@ let build_proof
 *)
   let proof, real_metasenv = 
     ProofEngineHelpers.subst_meta_and_metasenv_in_proof
-      proof goalno (CicMetaSubst.apply_subst final_subst) 
+      proof goalno final_subst
       (List.filter (fun i,_,_ -> i<>goalno ) real_menv)
   in      
   let open_goals = 
@@ -1568,7 +1568,7 @@ let pump_actives context bag maxm active passive saturation_steps max_time =
 let all_subsumed bag maxm status active passive =
   maxmeta := maxm;
   let proof, goalno = status in
-  let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
+  let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let env = metasenv,context,CicUniv.empty_ugraph in
   let cleaned_goal = Utils.remove_local_context type_of_goal in
@@ -1615,7 +1615,7 @@ let given_clause
   let mp = max_l passive_l in
 *)
   let proof, goalno = status in
-  let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
+  let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
   let cleaned_goal = Utils.remove_local_context type_of_goal in