From 50f0f051f84303b40f623ecd67cd0106c13c200a Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 24 Apr 2007 13:54:10 +0000 Subject: [PATCH] Subsumption_subst re-added to initial. --- components/tactics/paramodulation/saturation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2