From 7d62b9f665d208500d250ba422fedebdda48c718 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Thu, 29 Sep 2005 12:26:25 +0000 Subject: [PATCH] non-default equalities in equations_for_goal --- helm/ocaml/tactics/metadataQuery.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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 -- 2.39.2