ocaml 3.09 transition

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

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index c266502cb16fa50378252228c2f3c7af2e9dea7c..eaa146ed1d9cd71178fbc29c087a043529e17a9a 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -255,24 +255,49 @@ let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) =
   uris
 
 let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) =
+  let to_string set =
+    "{ " ^
+      (String.concat ", "
+         (Constr.UriManagerSet.fold
+            (fun u l -> (UriManager.string_of_uri u)::l) set []))
+    ^ " }"
+  in
  let (_, metasenv, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = Constr.signature_of ty in
- match main with
-     None -> raise Goal_is_not_an_equation
-   | Some (m,l) ->
-       if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then
-        let set = signature_of_hypothesis context in
-        let set = Constr.UriManagerSet.union set sig_constants in
-        let set = close_with_types set metasenv context in
-         let set = close_with_constructors set metasenv context in
-         let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in
-        let uris =
-          sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
-        let uris = List.filter nonvar (List.map snd uris) in
-        let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
-          uris
-       else raise Goal_is_not_an_equation
+(*  Printf.printf "\nsig_constants: %s\n\n" (to_string sig_constants); *)
+(*  match main with *)
+(*      None -> raise Goal_is_not_an_equation *)
+(*    | Some (m,l) -> *)
+ let m, l =
+   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
+   | Some (m, l) -> eq_URI, []
+ in
+ Printf.printf "\nSome (m, l): %s, [%s]\n\n"
+   (UriManager.string_of_uri m)
+   (String.concat "; " (List.map UriManager.string_of_uri 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); *)
+ let set = Constr.UriManagerSet.union set sig_constants in
+ let set = close_with_types set metasenv context in
+ (*          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 uris =
+   sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
+ let uris = List.filter nonvar (List.map snd uris) in
+ let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+ uris
+   (*        ) *)
+   (*        else raise Goal_is_not_an_equation *)
 
 let experimental_hint 
   ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =