X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=eaa146ed1d9cd71178fbc29c087a043529e17a9a;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=c266502cb16fa50378252228c2f3c7af2e9dea7c;hpb=259a4a2080cc5af5b20da1cd9133eb32f28c5d8f;p=helm.git

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index c266502cb..eaa146ed1 100644
--- 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) =