non-default equalities in equations_for_goal

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 6f6b2e00a68419b0e8ddfd179c6775e0e6c919cd..eaa146ed1d9cd71178fbc29c087a043529e17a9a 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -270,7 +270,10 @@ let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) =
 (*      None -> raise Goal_is_not_an_equation *)
 (*    | Some (m,l) -> *)
  let m, l =
-   let eq_URI = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI in
+   let eq_URI =
+     let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+     UriManager.uri_of_string (us ^ "#xpointer(1/1)")
+   in
    match main with
    | None -> eq_URI, []
    | Some (m, l) when UriManager.eq m eq_URI -> m, l