From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 12 Feb 2009 17:44:39 +0000 (+0000)
Subject: errata corrige.
X-Git-Tag: make_still_working~4203
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d990d5c64d0b9c07baef4257e7931321a42ae695;p=helm.git

errata corrige.
---

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 3b91f5f91..7cdbf43d3 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -1077,7 +1077,7 @@ let build_newg bag context goal rule expansion =
     in
     let name = Cic.Name "x" in     
     let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in 
-    let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
+    let newgoalproofstep = (rule,pos,id,subst,pred) in
     bo, (newgoalproofstep::goalproof)
   in
   let newmetasenv = (* Founif.filter subst *) menv in