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

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

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 3979c052985f76f542a68ad1c409ef8cf4274a44..3bff5b57460bc4decc952b913a83f4c410fb4d29 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/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