X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=eaa146ed1d9cd71178fbc29c087a043529e17a9a;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=6f6b2e00a68419b0e8ddfd179c6775e0e6c919cd;hpb=9547c888a55a5372ff2f6a2d2a9eab7d5d7c01fb;p=helm.git

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 6f6b2e00a..eaa146ed1 100644
--- 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