From: Andrea Asperti Date: Tue, 24 Apr 2007 13:54:10 +0000 (+0000) Subject: Subsumption_subst re-added to initial. X-Git-Tag: 0.4.95@7852~502 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=50f0f051f84303b40f623ecd67cd0106c13c200a;p=helm.git Subsumption_subst re-added to initial. --- diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index ff58512ea..f8b12c119 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/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