X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=3bff5b57460bc4decc952b913a83f4c410fb4d29;hb=08a92d276c5477968b02f31097b6ed03185f34eb;hp=3979c052985f76f542a68ad1c409ef8cf4274a44;hpb=9135f92fe15418abd2c2ae81ab155a2517bc72ea;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 3979c0529..3bff5b574 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -737,7 +737,7 @@ let build_goal_proof l initial ty se =
 let refl_proof ty term = 
   Cic.Appl 
     [Cic.MutConstruct 
-       (LibraryObjects.eq_URI (), 0, 1, []);
+       (Utils.eq_URI (), 0, 1, []);
        ty; term]
 ;;
 
@@ -912,14 +912,14 @@ let meta_convertibility t1 t2 =
 exception TermIsNotAnEquality;;
 
 let term_is_equality term =
-  let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
+  let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
   | _ -> false
 ;;
 
 let equality_of_term proof term =
-  let eq_uri = LibraryObjects.eq_URI () in
+  let eq_uri = Utils.eq_URI () in
   let iseq uri = UriManager.eq uri eq_uri in
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
@@ -951,7 +951,7 @@ let term_of_equality equality =
   let argsno = List.length menv in
   let t =
     CicSubstitution.lift argsno
-      (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
+      (Cic.Appl [Cic.MutInd (Utils.eq_URI (), 0, []); ty; left; right])
   in
   snd (
     List.fold_right