1. the default for the default equality/absurd/true/false URIs used to be

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

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index 6a21bb173d1f76f8cc380b56b4bd34160beed287..91fcee8a22833b645784a6e62ef03996e41d8f56 100644 (file)
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -211,7 +211,7 @@ let find_equalities context proof =
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
-  let eq_uri = LibraryObjects.eq_URI () in
+  let eq_uri = Utils.eq_URI () in
   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
   let ok_types ty menv =
     List.for_all (fun (_, _, mt) -> mt = ty) menv
@@ -349,7 +349,7 @@ let find_library_equalities dbd context status maxmeta =
        eqs)
   in
   let eq_uri1 = eq_XURI ()
-  and eq_uri2 = LibraryObjects.eq_URI () in
+  and eq_uri2 = Utils.eq_URI () in
   let iseq uri =
     (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
   in