From: Alberto Griggio <griggio@fbk.eu>
Date: Thu, 29 Sep 2005 12:26:25 +0000 (+0000)
Subject: non-default equalities in equations_for_goal
X-Git-Tag: V_0_7_2_3~277
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7d62b9f665d208500d250ba422fedebdda48c718;p=helm.git

non-default equalities in equations_for_goal
---

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