Dama is now in the night benchmarks.

[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..12c8e9bd65c6eb3a7ea6eadb2dd916db6b5e2494 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