...

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

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 546fff631b1a6bf855a410e6ed0df65a15ab7520..ff5bf23cbbaae16548a4dd6a643fa089856ec96c 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -601,8 +601,8 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
     | Some t ->
         let newmeta, newtarget = build_newtarget true t in
           assert (not (Equality.meta_convertibility_eq target newtarget));
-          if (Equality.is_weak_identity newtarget) ||
-            (Equality.meta_convertibility_eq target newtarget) then
+          if (Equality.is_weak_identity newtarget) (* || *)
+            (*Equality.meta_convertibility_eq target newtarget*) then
               newmeta, newtarget
           else 
             demodulation_equality bag ?from eq_uri newmeta env table newtarget
@@ -843,7 +843,7 @@ let superposition_right bag
   in
   let new1 = List.map (build_new U.Gt) res1
   and new2 = List.map (build_new U.Lt) res2 in
-  let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
+  let ok e = not (Equality.is_weak_identity (*metasenv', context, ugraph*) e) in
   (!maxmeta,
    (List.filter ok (new1 @ new2)))
 ;;