]> matita.cs.unibo.it Git - helm.git/commitdiff
Subsumption_subst re-added to initial.
authorAndrea Asperti <andrea.asperti@unibo.it>
Tue, 24 Apr 2007 13:54:10 +0000 (13:54 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Tue, 24 Apr 2007 13:54:10 +0000 (13:54 +0000)
helm/software/components/tactics/paramodulation/saturation.ml

index ff58512ea9d1f47c429d6f0f6b412fc5c96b4165..f8b12c11952051f3736ab24d314b6bc74aed15fd 100644 (file)
@@ -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