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 ff5bf23cbbaae16548a4dd6a643fa089856ec96c..12c8e9bd65c6eb3a7ea6eadb2dd916db6b5e2494 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -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_weak_identity (*metasenv', context, ugraph*) e) in
+  let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
   (!maxmeta,
    (List.filter ok (new1 @ new2)))
 ;;