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

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

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index a26ec0f73b40c5d9c4ae552655735b56919e7a8c..1282ed27f1cd9f9726baccb892c06dd3c73ee6fb 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -889,7 +889,7 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
 *)
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
-    when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
+    when UriManager.eq uri (Utils.eq_URI ()) ->
       (let goal_equation = 
          Equality.mk_equality
            (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Eq),menv) 
@@ -946,7 +946,7 @@ let rec given_clause_fullred dbd env goals theorems ~passive active =
 (*     in *)
     let ok, proof =
       (* apply_goal_to_theorems dbd env theorems ~passive active goals in *)
-      let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
+      let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in
       match fst goals with
         | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])::_ 
             when left = right && iseq uri -> 
@@ -1195,7 +1195,7 @@ let given_clause_fullred dbd env goals theorems passive active =
     (given_clause_fullred dbd env goals theorems passive) active
 *)
 
-let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ());;
+let iseq uri = UriManager.eq uri (Utils.eq_URI ());;
 
 let check_if_goal_is_identity env = function
   | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) 
@@ -1671,7 +1671,7 @@ let saturate
         context_hyp @ thms, []
       else
         let refl_equal =
-          let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+          let us = UriManager.string_of_uri (Utils.eq_URI ()) in
           UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
         in
         let t = CicUtil.term_of_uri refl_equal in