X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Findexing.ml;h=b535119ed2df5702e9c8a3f2f0a99ce4d0bd7b80;hb=06a089726af079d5b2fe42ba78632565dad0eb3e;hp=7bbc4d43ca7fb7548a6397f08ffc16f473d9c648;hpb=9ab7d3460c70ee067f75bf6523d06b67d6e7750a;p=helm.git

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index 7bbc4d43c..b535119ed 100644
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -655,7 +655,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
@@ -959,7 +959,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,8 +1003,11 @@ 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 name = Cic.Name "x" in
+    let bo' = (*apply_subst subst*) t in
+    (* patch?? 
+    let bo' = 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)
   in