There used to be two minimal joins between an ordered_set and an abelian_group:

[helm.git] / components / tactics / paramodulation / indexing.ml

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index 7bbc4d43ca7fb7548a6397f08ffc16f473d9c648..b535119ed2df5702e9c8a3f2f0a99ce4d0bd7b80 100644 (file)
--- 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