Apply patch-coq-8.0pl3-ocaml-3.09 patch.

3 files changed, 515 insertions, 0 deletions

diff --git a/debian/changelog b/debian/changelog
index 604ef988..80dde408 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,10 @@
+coq (8.0pl3-2) unstable; urgency=low
+
+  * Added coq-8.0pl3-ocaml-3.09.dpatch to avoid intuition to loop forever,
+    closes: #353493.
+
+ -- Samuel Mimram <smimram@debian.org>  Sun, 19 Feb 2006 11:33:21 +0000
+
 coq (8.0pl3-1) unstable; urgency=low
 
   * New upstream release.
diff --git a/debian/patches/00list b/debian/patches/00list
index e69de29b..3804c9ad 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -0,0 +1 @@
+coq-8.0pl3-ocaml-3.09
diff --git a/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch b/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch
new file mode 100755
index 00000000..90b4d583
--- /dev/null
+++ b/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch
@@ -0,0 +1,507 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## coq-8.0pl3-ocaml-3.09.dpatch by Samuel Mimram <smimram@debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Patch provided by coq's upstream to fix problems with OCaml 3.09.
+## DP: ftp://ftp.inria.fr/INRIA/coq/V8.0pl3/patch-coq-8.0pl3-ocaml-3.09
+
+@DPATCH@
+diff -urNad coq-8.0pl3~/Makefile coq-8.0pl3/Makefile
+--- coq-8.0pl3~/Makefile	2006-01-11 23:18:05.000000000 +0000
++++ coq-8.0pl3/Makefile	2006-02-19 11:28:43.000000000 +0000
+@@ -77,8 +77,8 @@
+ 
+ MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
+ 
+-BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG)
+-OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF)
++BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) -w y
++OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) -w y
+ OCAMLDEP=ocamldep
+ DEPFLAGS=-slash $(LOCALINCLUDES)
+ 
+diff -urNad coq-8.0pl3~/contrib/first-order/sequent.ml coq-8.0pl3/contrib/first-order/sequent.ml
+--- coq-8.0pl3~/contrib/first-order/sequent.ml	2004-07-16 19:30:10.000000000 +0000
++++ coq-8.0pl3/contrib/first-order/sequent.ml	2006-02-19 11:28:43.000000000 +0000
+@@ -6,7 +6,7 @@
+ (*         *       GNU Lesser General Public License Version 2.1        *)
+ (************************************************************************)
+ 
+-(* $Id: sequent.ml,v 1.17.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
++(* $Id: sequent.ml,v 1.17.2.2 2006/01/25 22:40:30 herbelin Exp $ *)
+ 
+ open Term
+ open Util
+@@ -278,7 +278,7 @@
+   let h dbname=
+     let hdb=
+       try
+-	Util.Stringmap.find dbname !searchtable 
++	searchtable_map dbname 
+       with Not_found-> 
+ 	error ("Firstorder: "^dbname^" : No such Hint database") in
+       Hint_db.iter g hdb in
+diff -urNad coq-8.0pl3~/contrib/interface/blast.ml coq-8.0pl3/contrib/interface/blast.ml
+--- coq-8.0pl3~/contrib/interface/blast.ml	2004-07-16 19:30:11.000000000 +0000
++++ coq-8.0pl3/contrib/interface/blast.ml	2006-02-19 11:28:43.000000000 +0000
+@@ -351,16 +351,16 @@
+   let db_list =
+     List.map
+       (fun x -> 
+-	 try Stringmap.find x !searchtable
++	 try searchtable_map x
+ 	 with Not_found -> error ("EAuto: "^x^": No such Hint database"))
+       ("core"::dbnames) 
+   in
+   tclTRY (e_search_auto debug np db_list)
+ 
+ let full_eauto debug n gl = 
+-  let dbnames = stringmap_dom !searchtable in
++  let dbnames = current_db_names () in
+   let dbnames =  list_subtract dbnames ["v62"] in
+-  let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
++  let db_list = List.map searchtable_map dbnames in
+   let local_db = make_local_hint_db gl in
+   tclTRY (e_search_auto debug n db_list) gl
+ 
+@@ -369,8 +369,6 @@
+ (**********************************************************************
+    copié de tactics/auto.ml on a juste modifié search_gen
+ *)
+-let searchtable_map name = 
+-  Stringmap.find name !searchtable
+ 
+ (* local_db is a Hint database containing the hypotheses of current goal *)
+ (* Papageno : cette fonction a été pas mal simplifiée depuis que la base
+@@ -499,9 +497,9 @@
+ let default_search_depth = ref 5
+ 			     
+ let full_auto n gl = 
+-  let dbnames = stringmap_dom !searchtable in
++  let dbnames = current_db_names () in
+   let dbnames = list_subtract dbnames ["v62"] in
+-  let db_list = List.map (fun x -> searchtable_map x) dbnames in
++  let db_list = List.map searchtable_map dbnames in
+   let hyps = pf_hyps gl in
+   tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
+   
+diff -urNad coq-8.0pl3~/interp/symbols.ml coq-8.0pl3/interp/symbols.ml
+--- coq-8.0pl3~/interp/symbols.ml	2004-11-17 09:33:38.000000000 +0000
++++ coq-8.0pl3/interp/symbols.ml	2006-02-19 11:28:43.000000000 +0000
+@@ -6,7 +6,7 @@
+ (*         *       GNU Lesser General Public License Version 2.1        *)
+ (************************************************************************)
+ 
+-(* $Id: symbols.ml,v 1.31.2.2 2004/11/17 09:33:38 herbelin Exp $ *)
++(* $Id: symbols.ml,v 1.31.2.3 2006/01/25 22:40:30 herbelin Exp $ *)
+ 
+ (*i*)
+ open Util
+@@ -43,18 +43,18 @@
+ type delimiters = string
+ 
+ type scope = {
+-  notations: (interpretation * (dir_path * string) * bool) Stringmap.t;
++  notations: (string, interpretation * (dir_path * string) * bool) Gmap.t;
+   delimiters: delimiters option
+ }
+ 
+ (* Uninterpreted notation map: notation -> level * dir_path *)
+-let notation_level_map = ref Stringmap.empty
++let notation_level_map = ref Gmap.empty
+ 
+ (* Scopes table: scope_name -> symbol_interpretation *)
+-let scope_map = ref Stringmap.empty
++let scope_map = ref Gmap.empty
+ 
+ let empty_scope = {
+-  notations = Stringmap.empty;
++  notations = Gmap.empty;
+   delimiters = None
+ }
+ 
+@@ -62,20 +62,20 @@
+ let type_scope = "type_scope" (* special scope used for interpreting types *)
+ 
+ let init_scope_map () =
+-  scope_map := Stringmap.add default_scope empty_scope !scope_map;
+-  scope_map := Stringmap.add type_scope empty_scope !scope_map
++  scope_map := Gmap.add default_scope empty_scope !scope_map;
++  scope_map := Gmap.add type_scope empty_scope !scope_map
+ 
+ (**********************************************************************)
+ (* Operations on scopes *)
+ 
+ let declare_scope scope =
+-  try let _ = Stringmap.find scope !scope_map in ()
++  try let _ = Gmap.find scope !scope_map in ()
+   with Not_found ->
+ (*    Options.if_verbose message ("Creating scope "^scope);*)
+-    scope_map := Stringmap.add scope empty_scope !scope_map
++    scope_map := Gmap.add scope empty_scope !scope_map
+ 
+ let find_scope scope =
+-  try Stringmap.find scope !scope_map
++  try Gmap.find scope !scope_map
+   with Not_found -> error ("Scope "^scope^" is not declared")
+ 
+ let check_scope sc = let _ = find_scope sc in ()
+@@ -124,7 +124,7 @@
+ (**********************************************************************)
+ (* Delimiters *)
+ 
+-let delimiters_map = ref Stringmap.empty
++let delimiters_map = ref Gmap.empty
+ 
+ let declare_delimiters scope key =
+   let sc = find_scope scope in
+@@ -134,15 +134,15 @@
+       warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
+   end;
+   let sc = { sc with delimiters = Some key } in
+-  scope_map := Stringmap.add scope sc !scope_map;
+-  if Stringmap.mem key !delimiters_map then begin
+-    let oldsc = Stringmap.find key !delimiters_map in
++  scope_map := Gmap.add scope sc !scope_map;
++  if Gmap.mem key !delimiters_map then begin
++    let oldsc = Gmap.find key !delimiters_map in
+     Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc)
+   end;
+-  delimiters_map := Stringmap.add key scope !delimiters_map
++  delimiters_map := Gmap.add key scope !delimiters_map
+ 
+ let find_delimiters_scope loc key = 
+-  try Stringmap.find key !delimiters_map
++  try Gmap.find key !delimiters_map
+   with Not_found -> 
+     user_err_loc 
+     (loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
+@@ -229,7 +229,7 @@
+ let find_with_delimiters = function
+   | None -> None
+   | Some scope ->
+-      match (Stringmap.find scope !scope_map).delimiters with
++      match (Gmap.find scope !scope_map).delimiters with
+ 	| Some key -> Some (Some scope, Some key)
+ 	| None -> None
+ 
+@@ -257,23 +257,23 @@
+ (* Uninterpreted notation levels *)
+ 
+ let declare_notation_level ntn level =
+-  if not !Options.v7 & Stringmap.mem ntn !notation_level_map then
++  if not !Options.v7 & Gmap.mem ntn !notation_level_map then
+     error ("Notation "^ntn^" is already assigned a level");
+-  notation_level_map := Stringmap.add ntn level !notation_level_map
++  notation_level_map := Gmap.add ntn level !notation_level_map
+ 
+ let level_of_notation ntn =
+-  Stringmap.find ntn !notation_level_map
++  Gmap.find ntn !notation_level_map
+ 
+ (* The mapping between notations and their interpretation *)
+ 
+ let declare_notation_interpretation ntn scopt pat df pp8only =
+   let scope = match scopt with Some s -> s | None -> default_scope in
+   let sc = find_scope scope in
+-  if Stringmap.mem ntn sc.notations && Options.is_verbose () then
++  if Gmap.mem ntn sc.notations && Options.is_verbose () then
+     warning ("Notation "^ntn^" was already used"^
+     (if scopt = None then "" else " in scope "^scope));
+-  let sc = { sc with notations = Stringmap.add ntn (pat,df,pp8only) sc.notations } in
+-  scope_map := Stringmap.add scope sc !scope_map;
++  let sc = { sc with notations = Gmap.add ntn (pat,df,pp8only) sc.notations } in
++  scope_map := Gmap.add scope sc !scope_map;
+   if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack
+ 
+ let declare_uninterpretation rule (metas,c as pat) =
+@@ -292,7 +292,7 @@
+ let rec interp_notation loc ntn scopes =
+   let f sc =
+     let scope = find_scope sc in
+-    let (pat,df,pp8only) = Stringmap.find ntn scope.notations in
++    let (pat,df,pp8only) = Gmap.find ntn scope.notations in
+     if pp8only then raise Not_found;
+     pat,(df,if sc = default_scope then None else Some sc) in
+   try find_interpretation f (List.fold_right push_scope scopes !scope_stack)
+@@ -308,7 +308,7 @@
+ 
+ let availability_of_notation (ntn_scope,ntn) scopes =
+   let f scope =
+-    Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
++    Gmap.mem ntn (Gmap.find scope !scope_map).notations in
+   find_without_delimiters f (ntn_scope,Some ntn) scopes
+ 
+ let rec interp_numeral_gen loc f n = function
+@@ -356,8 +356,8 @@
+ let exists_notation_in_scope scopt ntn r =
+   let scope = match scopt with Some s -> s | None -> default_scope in
+   try
+-    let sc = Stringmap.find scope !scope_map in
+-    let (r',_,pp8only) = Stringmap.find ntn sc.notations in
++    let sc = Gmap.find scope !scope_map in
++    let (r',_,pp8only) = Gmap.find ntn sc.notations in
+     r' = r, pp8only
+   with Not_found -> false, false
+ 
+@@ -487,14 +487,14 @@
+ 
+ let pr_named_scope prraw scope sc =
+  (if scope = default_scope then
+-   match Stringmap.fold (fun _ _ x -> x+1) sc.notations 0 with
++   match Gmap.fold (fun _ _ x -> x+1) sc.notations 0 with
+      | 0 -> str "No lonely notation"
+      | n -> str "Lonely notation" ++ (if n=1 then mt() else str"s")
+   else 
+     str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
+   ++ fnl ()
+   ++ pr_scope_classes scope
+-  ++ Stringmap.fold
++  ++ Gmap.fold
+        (fun ntn ((_,r),(_,df),_) strm ->
+ 	 pr_notation_info prraw df r ++ fnl () ++ strm)
+        sc.notations (mt ())
+@@ -502,12 +502,12 @@
+ let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
+ 
+ let pr_scopes prraw =
+- Stringmap.fold 
++ Gmap.fold 
+    (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
+    !scope_map (mt ())
+ 
+ let rec find_default ntn = function
+-  | Scope scope::_ when Stringmap.mem ntn (find_scope scope).notations ->
++  | Scope scope::_ when Gmap.mem ntn (find_scope scope).notations ->
+       Some scope
+   | SingleNotation ntn'::_ when ntn = ntn' -> Some default_scope
+   | _::scopes -> find_default ntn scopes
+@@ -531,9 +531,9 @@
+     if String.contains ntn ' ' then (=) ntn
+     else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in
+   let l =
+-    Stringmap.fold 
++    Gmap.fold 
+       (fun scope_name sc ->
+-	Stringmap.fold (fun ntn ((_,r),df,_) l ->
++	Gmap.fold (fun ntn ((_,r),df,_) l ->
+ 	  if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
+       map [] in
+   let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in
+@@ -560,7 +560,7 @@
+ 
+ let collect_notation_in_scope scope sc known =
+   assert (scope <> default_scope);
+-  Stringmap.fold
++  Gmap.fold
+     (fun ntn ((_,r),(_,df),_) (l,known as acc) ->
+       if List.mem ntn known then acc else ((df,r)::l,ntn::known))
+     sc.notations ([],known)
+@@ -578,7 +578,7 @@
+ 	  if List.mem ntn knownntn then (all,knownntn)
+ 	  else
+ 	    let ((_,r),(_,df),_) =
+-	      Stringmap.find ntn (find_scope default_scope).notations in
++	      Gmap.find ntn (find_scope default_scope).notations in
+ 	    let all' = match all with
+ 	      | (s,lonelyntn)::rest when s = default_scope ->
+ 		  (s,(df,r)::lonelyntn)::rest
+@@ -614,13 +614,13 @@
+ 
+ (* Concrete syntax for symbolic-extension table *)
+ let printing_rules = 
+-  ref (Stringmap.empty : unparsing_rule Stringmap.t)
++  ref (Gmap.empty : (string, unparsing_rule) Gmap.t)
+ 
+ let declare_notation_printing_rule ntn unpl =
+-  printing_rules := Stringmap.add ntn unpl !printing_rules
++  printing_rules := Gmap.add ntn unpl !printing_rules
+ 
+ let find_notation_printing_rule ntn =
+-  try Stringmap.find ntn !printing_rules
++  try Gmap.find ntn !printing_rules
+   with Not_found -> anomaly ("No printing rule found for "^ntn)
+ 
+ (**********************************************************************)
+@@ -644,13 +644,13 @@
+ let init () =
+   init_scope_map ();
+ (*
+-  scope_stack := Stringmap.empty
++  scope_stack := Gmap.empty
+   arguments_scope := Refmap.empty
+ *)
+-  notation_level_map := Stringmap.empty;
+-  delimiters_map := Stringmap.empty;
++  notation_level_map := Gmap.empty;
++  delimiters_map := Gmap.empty;
+   notations_key_table := Gmapl.empty;
+-  printing_rules := Stringmap.empty;
++  printing_rules := Gmap.empty;
+   class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
+ 
+ let _ = 
+diff -urNad coq-8.0pl3~/tactics/auto.ml coq-8.0pl3/tactics/auto.ml
+--- coq-8.0pl3~/tactics/auto.ml	2005-05-15 12:47:04.000000000 +0000
++++ coq-8.0pl3/tactics/auto.ml	2006-02-19 11:28:43.000000000 +0000
+@@ -6,7 +6,7 @@
+ (*         *       GNU Lesser General Public License Version 2.1        *)
+ (************************************************************************)
+ 
+-(* $Id: auto.ml,v 1.63.2.3 2005/05/15 12:47:04 herbelin Exp $ *)
++(* $Id: auto.ml,v 1.63.2.4 2006/01/25 22:40:29 herbelin Exp $ *)
+ 
+ open Pp
+ open Util
+@@ -134,24 +134,28 @@
+ 
+ end
+ 
+-type frozen_hint_db_table = Hint_db.t Stringmap.t 
++module Hintdbmap = Gmap
+ 
+-type hint_db_table = Hint_db.t Stringmap.t ref
++type frozen_hint_db_table = (string,Hint_db.t) Hintdbmap.t 
++
++type hint_db_table = (string,Hint_db.t) Hintdbmap.t ref
+ 
+ type hint_db_name = string
+ 
+-let searchtable = (ref Stringmap.empty : hint_db_table)
++let searchtable = (ref Hintdbmap.empty : hint_db_table)
+ 
+ let searchtable_map name = 
+-  Stringmap.find name !searchtable
++  Hintdbmap.find name !searchtable
+ let searchtable_add (name,db) = 
+-  searchtable := Stringmap.add name db !searchtable
++  searchtable := Hintdbmap.add name db !searchtable
++let current_db_names () =
++  Hintdbmap.dom !searchtable
+ 
+ (**************************************************************************)
+ (*                       Definition of the summary                        *)
+ (**************************************************************************)
+ 
+-let init     () = searchtable := Stringmap.empty
++let init     () = searchtable := Hintdbmap.empty
+ let freeze   () = !searchtable
+ let unfreeze fs = searchtable := fs
+ 
+@@ -498,7 +502,7 @@
+ 
+ (* Print all hints associated to head c in any database *)
+ let fmt_hint_list_for_head c = 
+-  let dbs = stringmap_to_list !searchtable in
++  let dbs = Hintdbmap.to_list !searchtable in
+   let valid_dbs = 
+     map_succeed 
+       (fun (name,db) -> (name,db,Hint_db.map_all c db)) 
+@@ -523,7 +527,7 @@
+       | [] -> assert false 
+     in
+     let hd = head_of_constr_reference hdc in
+-    let dbs = stringmap_to_list !searchtable in
++    let dbs = Hintdbmap.to_list !searchtable in
+     let valid_dbs = 
+       if occur_existential cl then 
+ 	map_succeed 
+@@ -568,7 +572,7 @@
+   
+ (* displays all the hints of all databases *)
+ let print_searchtable () =
+-  Stringmap.iter
++  Hintdbmap.iter
+     (fun name db ->
+        msg (str "In the database " ++ str name ++ fnl ());
+        print_hint_db db)
+@@ -693,7 +697,7 @@
+   tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl 
+     
+ let full_trivial gl =
+-  let dbnames = stringmap_dom !searchtable in
++  let dbnames = Hintdbmap.dom !searchtable in
+   let dbnames = list_subtract dbnames ["v62"] in
+   let db_list = List.map (fun x -> searchtable_map x) dbnames in
+   tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl
+@@ -798,7 +802,7 @@
+ let default_auto = auto !default_search_depth []
+ 
+ let full_auto n gl = 
+-  let dbnames = stringmap_dom !searchtable in
++  let dbnames = Hintdbmap.dom !searchtable in
+   let dbnames = list_subtract dbnames ["v62"] in
+   let db_list = List.map (fun x -> searchtable_map x) dbnames in
+   let hyps = pf_hyps gl in
+@@ -911,7 +915,7 @@
+       to_add empty_named_context in
+   let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
+   let db = Hint_db.add_list db0 (make_local_hint_db g) in
+-  super_search n [Stringmap.find "core" !searchtable] db argl g
++  super_search n [Hintdbmap.find "core" !searchtable] db argl g
+ 
+ let superauto n to_add argl  = 
+   tclTRY (tclCOMPLETE (search_superauto n to_add argl))
+diff -urNad coq-8.0pl3~/tactics/auto.mli coq-8.0pl3/tactics/auto.mli
+--- coq-8.0pl3~/tactics/auto.mli	2005-01-21 16:41:52.000000000 +0000
++++ coq-8.0pl3/tactics/auto.mli	2006-02-19 11:28:43.000000000 +0000
+@@ -6,7 +6,7 @@
+ (*         *       GNU Lesser General Public License Version 2.1        *)
+ (************************************************************************)
+ 
+-(*i $Id: auto.mli,v 1.22.2.2 2005/01/21 16:41:52 herbelin Exp $ i*)
++(*i $Id: auto.mli,v 1.22.2.3 2006/01/25 22:40:29 herbelin Exp $ i*)
+ 
+ (*i*)
+ open Util
+@@ -56,12 +56,16 @@
+     val iter : (constr_label -> stored_data list -> unit) -> t -> unit
+   end
+ 
+-type frozen_hint_db_table = Hint_db.t Stringmap.t
++type frozen_hint_db_table
+ 
+-type hint_db_table = Hint_db.t Stringmap.t ref
++type hint_db_table
+ 
+ type hint_db_name = string
+ 
++val searchtable_map : hint_db_name -> Hint_db.t
++
++val current_db_names : unit -> hint_db_name list
++
+ val add_hints : locality_flag -> hint_db_name list -> hints -> unit
+ 
+ val print_searchtable : unit -> unit
+diff -urNad coq-8.0pl3~/tactics/eauto.ml4 coq-8.0pl3/tactics/eauto.ml4
+--- coq-8.0pl3~/tactics/eauto.ml4	2004-07-16 19:30:52.000000000 +0000
++++ coq-8.0pl3/tactics/eauto.ml4	2006-02-19 11:28:43.000000000 +0000
+@@ -8,7 +8,7 @@
+ 
+ (*i camlp4deps: "parsing/grammar.cma" i*)
+ 
+-(* $Id: eauto.ml4,v 1.11.2.1 2004/07/16 19:30:52 herbelin Exp $ *)
++(* $Id: eauto.ml4,v 1.11.2.2 2006/01/25 22:40:29 herbelin Exp $ *)
+ 
+ open Pp
+ open Util
+@@ -391,16 +391,16 @@
+   let db_list =
+     List.map
+       (fun x -> 
+-	 try Stringmap.find x !searchtable
++	 try searchtable_map x
+ 	 with Not_found -> error ("EAuto: "^x^": No such Hint database"))
+       ("core"::dbnames) 
+   in
+   tclTRY (e_search_auto debug np db_list)
+ 
+ let full_eauto debug n gl = 
+-  let dbnames = stringmap_dom !searchtable in
++  let dbnames = current_db_names () in
+   let dbnames =  list_subtract dbnames ["v62"] in
+-  let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
++  let db_list = List.map (fun x -> searchtable_map x) dbnames in
+   let local_db = make_local_hint_db gl in
+   tclTRY (e_search_auto debug n db_list) gl
+