1. the default for the default equality/absurd/true/false URIs used to be

[helm.git] / components / tactics / metadataQuery.ml

diff --git a/components/tactics/metadataQuery.ml b/components/tactics/metadataQuery.ml
index b9c0536538e4295726347b7ad82071e1c89ed160..8822c527c122b1caeb6e125ed999f14d90b20d2f 100644 (file)
--- a/components/tactics/metadataQuery.ml
+++ b/components/tactics/metadataQuery.ml
@@ -205,19 +205,22 @@ let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
 (*  match main with *)
 (*      None -> raise Goal_is_not_an_equation *)
 (*    | Some (m,l) -> *)
- let m, l =
+ let l =
    let eq_URI =
-     let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
-     UriManager.uri_of_string (us ^ "#xpointer(1/1)")
+    match LibraryObjects.eq_URI () with
+       None -> None
+     | Some s ->
+        Some
+         (UriManager.uri_of_string
+          (UriManager.string_of_uri s ^ "#xpointer(1/1)"))
    in
-   match main with
-   | None -> eq_URI, []
-   | Some (m, l) when UriManager.eq m eq_URI -> m, l
-   | Some (m, l) -> eq_URI, []
+   match eq_URI,main with
+   | Some eq_URI, Some (m, l) when UriManager.eq m eq_URI -> m::l
+   | _,_ -> []
  in
  Printf.printf "\nSome (m, l): %s, [%s]\n\n"
-   (UriManager.string_of_uri m)
-   (String.concat "; " (List.map UriManager.string_of_uri l));
+   (UriManager.string_of_uri (List.hd l))
+   (String.concat "; " (List.map UriManager.string_of_uri (List.tl l)));
  (*        if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *)
  let set = signature_of_hypothesis context in
  (*          Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *)
@@ -226,7 +229,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
  (*          Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *)
  let set = close_with_constructors set metasenv context in
  (*          Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *)
- let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in
+ let set = List.fold_right Constr.UriManagerSet.remove l set in
  let uris =
    sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
  let uris = List.filter nonvar (List.map snd uris) in