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

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index 28c22a64e..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 = 
@@ -655,7 +656,7 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
     match res with
     | Some t ->
         let newmeta, newtarget = build_newtarget true t in
-          assert (not (Equality.meta_convertibility_eq target newtarget));
+          (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
           if (Equality.is_weak_identity newtarget) (* || *)
             (*Equality.meta_convertibility_eq target newtarget*) then
               newmeta, newtarget
@@ -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' =
@@ -959,7 +961,7 @@ let rec demodulation_theorem bag newmeta env table theorem =
 let open_goal g =
   match g with
   | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) -> 
-      assert (LibraryObjects.is_eq_URI uri);
+      (* assert (LibraryObjects.is_eq_URI uri); *)
       proof,menv,eq,ty,l,r
   | _ -> assert false
 ;;
@@ -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)