From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 12 Feb 2009 11:38:54 +0000 (+0000)
Subject: Fixed a problem of lifting.
X-Git-Tag: make_still_working~4204
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5338da4d7047b18aacd43447a3261b531895291d;p=helm.git

Fixed a problem of lifting.
---

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