From 4e0ce221e8f218bbf60885173d61ea6ff9324213 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. --- helm/software/components/tactics/paramodulation/saturation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index ff58512ea..f8b12c119 100644 --- 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 -- 2.39.2