Hint repaired (an erroneous commit by myself).

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index f26dae805be9e085a6a8d6d3d58ae7b4265c92c8..fc5328e9ffa3c252267d44b77e2d1b21614a02ac 100644 (file)
--- 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 ->