Subsumption_subst must be applied to the initial proof before passing

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

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index b3a53d92953f61e2f86dad7baf146deab69dec79..2b3bcc0692d5d44d007d6e063747cc0bfbdb5fb2 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -1223,7 +1223,7 @@ let simplify_goal_set env goals passive active =
       (fun acc goal -> 
         match simplify_goal env goal ~passive active with 
         | _, g -> if find g acc then acc else g::acc)
-      [] active_goals
+      active_goals active_goals
   in
   if List.length active_goals <>  List.length simplified then
     prerr_endline "SEMPLIFICANDO HO SCARTATO...";
@@ -1723,11 +1723,12 @@ let saturate
             ~newmetasenv:metasenv ~oldmetasenv:proof_menv)
       in
       let goal_proof, side_effects_t = 
-        let initial = newproof in
+        let initial = Equality.add_subst subsumption_subst newproof in
         Equality.build_goal_proof goalproof initial type_of_goal side_effects
       in
 (*prerr_endline (CicPp.pp goal_proof names);*)
-      let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
+      (* ?? *)
+      let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in
       let side_effects_t = 
         List.map (Subst.apply_subst subsumption_subst) side_effects_t
       in