From d990d5c64d0b9c07baef4257e7931321a42ae695 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 12 Feb 2009 17:44:39 +0000 Subject: [PATCH] errata corrige. --- helm/software/components/tactics/paramodulation/indexing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2