Fixed a problem of lifting.

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