X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2Fparamodulation%2Findexing.ml;h=e72ed64dad3c37c9620a97ec7576784bf3cb80ae;hb=ec7717f5e0dd4c295ba1cfd57a0a6a46170490ef;hp=9c5ea281b9fbc65509f36488cfdd98597b279bc0;hpb=9de7ac55904a21812fbf1da5dacc7722c489362e;p=helm.git

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index 9c5ea281b..e72ed64da 100644
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -583,7 +583,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
       let name = C.Name "x" in
       let bo' =
         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
-          C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+          C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
                   S.lift 1 eq_ty; l; r]
       in
       if sign = Utils.Positive then
@@ -900,7 +900,7 @@ let superposition_right
       let bo'' =
         let l, r =
           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
-        C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+        C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
                 S.lift 1 eq_ty; l; r]
       in
       bo',