X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Findexing.ml;h=e453d95c12c968a3cd696b157db950a6f87408e7;hb=2a8919be0dddc9e97584d4e7823da021eac60870;hp=b535119ed2df5702e9c8a3f2f0a99ce4d0bd7b80;hpb=cab46a693418cb8a797bcaf8bb026dc1ba9b32d6;p=helm.git

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index b535119ed..e453d95c1 100644
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -621,6 +621,7 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
       with CicUtil.Meta_not_found _ -> ty
     in
+    let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newproof =
       let bo = 
@@ -858,6 +859,7 @@ let superposition_right bag
       Equality.open_equality  equality in
     let what, other = if pos = Utils.Left then what, other else other, what in
 
+    let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
     let newgoal, newproof =
       (* qua *)
       let bo' =
@@ -1003,10 +1005,8 @@ 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
-    (* patch?? 
-    let bo' = t in
-    let ty = apply_subst subst ty 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
     bo, (newgoalproofstep::goalproof)