(* 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