From 72232ba3f75b569d20c8c1af9907740a47c860da Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 20 May 2005 09:13:34 +0000 Subject: [PATCH] Hint repaired (an erroneous commit by myself). --- helm/ocaml/tactics/metadataQuery.ml | 13 +------------ 1 file changed, 1 insertion(+), 12 deletions(-) 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 -> -- 2.39.2