From 5338da4d7047b18aacd43447a3261b531895291d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 12 Feb 2009 11:38:54 +0000 Subject: [PATCH] Fixed a problem of lifting. --- .../components/tactics/paramodulation/indexing.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index 77a377a88..3b91f5f91 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -1075,9 +1075,8 @@ let build_newg bag context goal rule expansion = Utils.guarded_simpl context (apply_subst subst (CicSubstitution.subst other t)) in - let bo' = apply_subst subst t in - let ty = apply_subst subst ty in - let name = Cic.Name "x" 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 bo, (newgoalproofstep::goalproof) in @@ -1150,10 +1149,9 @@ let build_newgoal bag context goal posu rule expansion = Utils.guarded_simpl context (apply_subst subst (CicSubstitution.subst other t)) in - let bo' = apply_subst subst t in - let ty = apply_subst subst ty in let name = Cic.Name "x" in - let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in + let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in + let newgoalproofstep = (rule,pos,id,subst,pred) in bo, (newgoalproofstep::goalproof) in let newmetasenv = (* Founif.filter subst *) menv in @@ -1178,6 +1176,8 @@ let superposition_left bag (metasenv, context, ugraph) table goal maxmeta = prerr_endline (string_of_int (List.length expansionsl)); prerr_endline (string_of_int (List.length expansionsr)); *) + if expansionsl <> [] then prerr_endline "expansionl"; + if expansionsr <> [] then prerr_endline "expansionr"; List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl @ List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr -- 2.39.2