X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=fc5328e9ffa3c252267d44b77e2d1b21614a02ac;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=f26dae805be9e085a6a8d6d3d58ae7b4265c92c8;hpb=87955f4aa47c0f5f416f24bae4848eccb1cc23d5;p=helm.git

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index f26dae805..fc5328e9f 100644
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -250,17 +250,6 @@ let experimental_hint
   ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let (_, metasenv, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
-  let uris = 
-    if facts then
-      ["cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"]
-    else
-      ["cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
-       (* "cic:/Coq/Init/Logic/trans_eq.con"; *)
-       "cic:/Coq/Init/Logic/f_equal.con";
-       "cic:/Coq/Init/Logic/f_equal2.con";
-       "cic:/Coq/Init/Logic/f_equal3.con"] 
-  in
-  (* 
   let (uris, (main, sig_constants)) =
     match signature with
     | Some signature -> 
@@ -312,7 +301,7 @@ let experimental_hint
       filter_uris_forward ~dbd (main, other_constants) uris
     end else
       filter_uris_backward ~dbd ~facts (main, other_constants) uris
-  in *)
+  in 
   let rec aux = function
     | [] -> []
     | uri :: tl ->