upgraded code to work with non-default equalities

[helm.git] / helm / ocaml / paramodulation / saturation.ml

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index bc935d7f730c518d97ed9c3a7dba09ba03c64714..4cf14ae18a4baf579c13e8f54db8d8f68d57b962 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -875,7 +875,8 @@ let apply_equality_to_goal env equality goal =
   let module I = Inference in
   let metasenv, context, ugraph = env in
   let _, proof, (ty, left, right, _), metas, args = equality in
-  let eqterm = C.Appl [C.MutInd (HL.Logic.eq_URI, 0, []); ty; left; right] in
+  let eqterm =
+    C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in
   let gproof, gmetas, gterm = goal in
   try
     let subst, metasenv', _ =
@@ -1969,7 +1970,8 @@ let saturate
         context_hyp @ thms
       else
         let refl_equal =
-          UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"
+          let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+          UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
         in
         let t = CicUtil.term_of_uri refl_equal in
         let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in