errata corrige.

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 3b91f5f91c1cf67ae6c87c46cf72a451c7ab4eb8..7cdbf43d38a2242938c5f83c710f08f3cfe08761 100644 (file)
--- 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