Subsumption_subst re-added to initial.

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index ff58512ea9d1f47c429d6f0f6b412fc5c96b4165..f8b12c11952051f3736ab24d314b6bc74aed15fd 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1338,7 +1338,7 @@ let build_proof
       (ProofEngineHelpers.compare_metasenvs 
          ~newmetasenv:metasenv ~oldmetasenv:proof_menv) in
   let goal_proof, side_effects_t = 
-    let initial = (* Equality.add_subst subsumption_subst*) newproof in
+    let initial = Equality.add_subst subsumption_subst newproof in
       Equality.build_goal_proof bag
         eq_uri goalproof initial type_of_goal side_effects
         context proof_menv