Index: Makefile
===================================================================
RCS file: /net/pauillac/constr/ARCHIVE/CONSTR/V7/Makefile,v
retrieving revision 1.459.2.22
diff -c -r1.459.2.22 Makefile
*** Makefile	2006/01/11 23:18:05	1.459.2.22
--- Makefile	2006/01/30 12:31:38
***************
*** 77,84 ****
  
  MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
  
! BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG)
! OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF)
  OCAMLDEP=ocamldep
  DEPFLAGS=-slash $(LOCALINCLUDES)
  
--- 77,84 ----
  
  MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
  
! BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) -w y
! OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) -w y
  OCAMLDEP=ocamldep
  DEPFLAGS=-slash $(LOCALINCLUDES)
  
Index: contrib/first-order/sequent.ml
===================================================================
RCS file: /net/pauillac/constr/ARCHIVE/CONSTR/V7/contrib/first-order/sequent.ml,v
retrieving revision 1.17.2.1
retrieving revision 1.17.2.2
diff -c -r1.17.2.1 -r1.17.2.2
*** contrib/first-order/sequent.ml	2004/07/16 19:30:10	1.17.2.1
--- contrib/first-order/sequent.ml	2006/01/25 22:40:30	1.17.2.2
***************
*** 6,12 ****
  (*         *       GNU Lesser General Public License Version 2.1        *)
  (************************************************************************)
  
! (* $Id: sequent.ml,v 1.17.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
  
  open Term
  open Util
--- 6,12 ----
  (*         *       GNU Lesser General Public License Version 2.1        *)
  (************************************************************************)
  
! (* $Id: sequent.ml,v 1.17.2.2 2006/01/25 22:40:30 herbelin Exp $ *)
  
  open Term
  open Util
***************
*** 278,284 ****
    let h dbname=
      let hdb=
        try
! 	Util.Stringmap.find dbname !searchtable 
        with Not_found-> 
  	error ("Firstorder: "^dbname^" : No such Hint database") in
        Hint_db.iter g hdb in
--- 278,284 ----
    let h dbname=
      let hdb=
        try
! 	searchtable_map dbname 
        with Not_found-> 
  	error ("Firstorder: "^dbname^" : No such Hint database") in
        Hint_db.iter g hdb in
Index: contrib/interface/blast.ml
===================================================================
RCS file: /net/pauillac/constr/ARCHIVE/CONSTR/V7/contrib/interface/blast.ml,v
retrieving revision 1.9.2.1
retrieving revision 1.9.2.2
diff -c -r1.9.2.1 -r1.9.2.2
*** contrib/interface/blast.ml	2004/07/16 19:30:11	1.9.2.1
--- contrib/interface/blast.ml	2006/01/25 22:40:30	1.9.2.2
***************
*** 351,366 ****
    let db_list =
      List.map
        (fun x -> 
! 	 try Stringmap.find x !searchtable
  	 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 =  list_subtract dbnames ["v62"] in
!   let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
    let local_db = make_local_hint_db gl in
    tclTRY (e_search_auto debug n db_list) gl
  
--- 351,366 ----
    let db_list =
      List.map
        (fun x -> 
! 	 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 = current_db_names () in
    let dbnames =  list_subtract dbnames ["v62"] 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,376 ****
  (**********************************************************************
     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
--- 369,374 ----
***************
*** 499,507 ****
  let default_search_depth = ref 5
  			     
  let full_auto n gl = 
!   let dbnames = stringmap_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
    tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
    
--- 497,505 ----
  let default_search_depth = ref 5
  			     
  let full_auto n gl = 
!   let dbnames = current_db_names () in
    let dbnames = list_subtract dbnames ["v62"] 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
    
Index: interp/symbols.ml
===================================================================
RCS file: /net/pauillac/constr/ARCHIVE/CONSTR/V7/interp/Attic/symbols.ml,v
retrieving revision 1.31.2.2
retrieving revision 1.31.2.3
diff -c -r1.31.2.2 -r1.31.2.3
*** interp/symbols.ml	2004/11/17 09:33:38	1.31.2.2
--- interp/symbols.ml	2006/01/25 22:40:30	1.31.2.3
***************
*** 6,12 ****
  (*         *       GNU Lesser General Public License Version 2.1        *)
  (************************************************************************)
  
! (* $Id: symbols.ml,v 1.31.2.2 2004/11/17 09:33:38 herbelin Exp $ *)
  
  (*i*)
  open Util
--- 6,12 ----
  (*         *       GNU Lesser General Public License Version 2.1        *)
  (************************************************************************)
  
! (* $Id: symbols.ml,v 1.31.2.3 2006/01/25 22:40:30 herbelin Exp $ *)
  
  (*i*)
  open Util
***************
*** 43,60 ****
  type delimiters = string
  
  type scope = {
!   notations: (interpretation * (dir_path * string) * bool) Stringmap.t;
    delimiters: delimiters option
  }
  
  (* Uninterpreted notation map: notation -> level * dir_path *)
! let notation_level_map = ref Stringmap.empty
  
  (* Scopes table: scope_name -> symbol_interpretation *)
! let scope_map = ref Stringmap.empty
  
  let empty_scope = {
!   notations = Stringmap.empty;
    delimiters = None
  }
  
--- 43,60 ----
  type delimiters = string
  
  type scope = {
!   notations: (string, interpretation * (dir_path * string) * bool) Gmap.t;
    delimiters: delimiters option
  }
  
  (* Uninterpreted notation map: notation -> level * dir_path *)
! let notation_level_map = ref Gmap.empty
  
  (* Scopes table: scope_name -> symbol_interpretation *)
! let scope_map = ref Gmap.empty
  
  let empty_scope = {
!   notations = Gmap.empty;
    delimiters = None
  }
  
***************
*** 62,81 ****
  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
  
  (**********************************************************************)
  (* Operations on scopes *)
  
  let declare_scope scope =
!   try let _ = Stringmap.find scope !scope_map in ()
    with Not_found ->
  (*    Options.if_verbose message ("Creating scope "^scope);*)
!     scope_map := Stringmap.add scope empty_scope !scope_map
  
  let find_scope scope =
!   try Stringmap.find scope !scope_map
    with Not_found -> error ("Scope "^scope^" is not declared")
  
  let check_scope sc = let _ = find_scope sc in ()
--- 62,81 ----
  let type_scope = "type_scope" (* special scope used for interpreting types *)
  
  let init_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 _ = Gmap.find scope !scope_map in ()
    with Not_found ->
  (*    Options.if_verbose message ("Creating scope "^scope);*)
!     scope_map := Gmap.add scope empty_scope !scope_map
  
  let find_scope scope =
!   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,130 ****
  (**********************************************************************)
  (* Delimiters *)
  
! let delimiters_map = ref Stringmap.empty
  
  let declare_delimiters scope key =
    let sc = find_scope scope in
--- 124,130 ----
  (**********************************************************************)
  (* Delimiters *)
  
! let delimiters_map = ref Gmap.empty
  
  let declare_delimiters scope key =
    let sc = find_scope scope in
***************
*** 134,148 ****
        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
      Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc)
    end;
!   delimiters_map := Stringmap.add key scope !delimiters_map
  
  let find_delimiters_scope loc key = 
!   try Stringmap.find key !delimiters_map
    with Not_found -> 
      user_err_loc 
      (loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
--- 134,148 ----
        warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
    end;
    let sc = { sc with delimiters = Some key } 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 := Gmap.add key scope !delimiters_map
  
  let find_delimiters_scope loc key = 
!   try Gmap.find key !delimiters_map
    with Not_found -> 
      user_err_loc 
      (loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
***************
*** 229,235 ****
  let find_with_delimiters = function
    | None -> None
    | Some scope ->
!       match (Stringmap.find scope !scope_map).delimiters with
  	| Some key -> Some (Some scope, Some key)
  	| None -> None
  
--- 229,235 ----
  let find_with_delimiters = function
    | None -> None
    | Some scope ->
!       match (Gmap.find scope !scope_map).delimiters with
  	| Some key -> Some (Some scope, Some key)
  	| None -> None
  
***************
*** 257,279 ****
  (* Uninterpreted notation levels *)
  
  let declare_notation_level ntn level =
!   if not !Options.v7 & Stringmap.mem ntn !notation_level_map then
      error ("Notation "^ntn^" is already assigned a level");
!   notation_level_map := Stringmap.add ntn level !notation_level_map
  
  let level_of_notation ntn =
!   Stringmap.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
      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;
    if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack
  
  let declare_uninterpretation rule (metas,c as pat) =
--- 257,279 ----
  (* Uninterpreted notation levels *)
  
  let declare_notation_level ntn level =
!   if not !Options.v7 & Gmap.mem ntn !notation_level_map then
      error ("Notation "^ntn^" is already assigned a level");
!   notation_level_map := Gmap.add ntn level !notation_level_map
  
  let level_of_notation ntn =
!   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 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 = 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,298 ****
  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
      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)
--- 292,298 ----
  let rec interp_notation loc ntn scopes =
    let f sc =
      let scope = find_scope sc 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,314 ****
  
  let availability_of_notation (ntn_scope,ntn) scopes =
    let f scope =
!     Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
    find_without_delimiters f (ntn_scope,Some ntn) scopes
  
  let rec interp_numeral_gen loc f n = function
--- 308,314 ----
  
  let availability_of_notation (ntn_scope,ntn) scopes =
    let f scope =
!     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,363 ****
  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
      r' = r, pp8only
    with Not_found -> false, false
  
--- 356,363 ----
  let exists_notation_in_scope scopt ntn r =
    let scope = match scopt with Some s -> s | None -> default_scope in
    try
!     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,500 ****
  
  let pr_named_scope prraw scope sc =
   (if scope = default_scope then
!    match Stringmap.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
         (fun ntn ((_,r),(_,df),_) strm ->
  	 pr_notation_info prraw df r ++ fnl () ++ strm)
         sc.notations (mt ())
--- 487,500 ----
  
  let pr_named_scope prraw scope sc =
   (if scope = default_scope then
!    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
!   ++ Gmap.fold
         (fun ntn ((_,r),(_,df),_) strm ->
  	 pr_notation_info prraw df r ++ fnl () ++ strm)
         sc.notations (mt ())
***************
*** 502,513 ****
  let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
  
  let pr_scopes prraw =
!  Stringmap.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 ->
        Some scope
    | SingleNotation ntn'::_ when ntn = ntn' -> Some default_scope
    | _::scopes -> find_default ntn scopes
--- 502,513 ----
  let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
  
  let pr_scopes prraw =
!  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 Gmap.mem ntn (find_scope scope).notations ->
        Some scope
    | SingleNotation ntn'::_ when ntn = ntn' -> Some default_scope
    | _::scopes -> find_default ntn scopes
***************
*** 531,539 ****
      if String.contains ntn ' ' then (=) ntn
      else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in
    let l =
!     Stringmap.fold 
        (fun scope_name sc ->
! 	Stringmap.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
--- 531,539 ----
      if String.contains ntn ' ' then (=) ntn
      else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in
    let l =
!     Gmap.fold 
        (fun scope_name sc ->
! 	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,566 ****
  
  let collect_notation_in_scope scope sc known =
    assert (scope <> default_scope);
!   Stringmap.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)
--- 560,566 ----
  
  let collect_notation_in_scope scope sc known =
    assert (scope <> default_scope);
!   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,584 ****
  	  if List.mem ntn knownntn then (all,knownntn)
  	  else
  	    let ((_,r),(_,df),_) =
! 	      Stringmap.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
--- 578,584 ----
  	  if List.mem ntn knownntn then (all,knownntn)
  	  else
  	    let ((_,r),(_,df),_) =
! 	      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,626 ****
  
  (* Concrete syntax for symbolic-extension table *)
  let printing_rules = 
!   ref (Stringmap.empty : unparsing_rule Stringmap.t)
  
  let declare_notation_printing_rule ntn unpl =
!   printing_rules := Stringmap.add ntn unpl !printing_rules
  
  let find_notation_printing_rule ntn =
!   try Stringmap.find ntn !printing_rules
    with Not_found -> anomaly ("No printing rule found for "^ntn)
  
  (**********************************************************************)
--- 614,626 ----
  
  (* Concrete syntax for symbolic-extension table *)
  let printing_rules = 
!   ref (Gmap.empty : (string, unparsing_rule) Gmap.t)
  
  let declare_notation_printing_rule ntn unpl =
!   printing_rules := Gmap.add ntn unpl !printing_rules
  
  let find_notation_printing_rule ntn =
!   try Gmap.find ntn !printing_rules
    with Not_found -> anomaly ("No printing rule found for "^ntn)
  
  (**********************************************************************)
***************
*** 644,656 ****
  let init () =
    init_scope_map ();
  (*
!   scope_stack := Stringmap.empty
    arguments_scope := Refmap.empty
  *)
!   notation_level_map := Stringmap.empty;
!   delimiters_map := Stringmap.empty;
    notations_key_table := Gmapl.empty;
!   printing_rules := Stringmap.empty;
    class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
  
  let _ = 
--- 644,656 ----
  let init () =
    init_scope_map ();
  (*
!   scope_stack := Gmap.empty
    arguments_scope := Refmap.empty
  *)
!   notation_level_map := Gmap.empty;
!   delimiters_map := Gmap.empty;
    notations_key_table := Gmapl.empty;
!   printing_rules := Gmap.empty;
    class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
  
  let _ = 
Index: tactics/auto.ml
===================================================================
RCS file: /net/pauillac/constr/ARCHIVE/CONSTR/V7/tactics/auto.ml,v
retrieving revision 1.63.2.3
retrieving revision 1.63.2.4
diff -c -r1.63.2.3 -r1.63.2.4
*** tactics/auto.ml	2005/05/15 12:47:04	1.63.2.3
--- tactics/auto.ml	2006/01/25 22:40:29	1.63.2.4
***************
*** 6,12 ****
  (*         *       GNU Lesser General Public License Version 2.1        *)
  (************************************************************************)
  
! (* $Id: auto.ml,v 1.63.2.3 2005/05/15 12:47:04 herbelin Exp $ *)
  
  open Pp
  open Util
--- 6,12 ----
  (*         *       GNU Lesser General Public License Version 2.1        *)
  (************************************************************************)
  
! (* $Id: auto.ml,v 1.63.2.4 2006/01/25 22:40:29 herbelin Exp $ *)
  
  open Pp
  open Util
***************
*** 134,157 ****
  
  end
  
! type frozen_hint_db_table = Hint_db.t Stringmap.t 
  
! type hint_db_table = Hint_db.t Stringmap.t ref
  
  type hint_db_name = string
  
! let searchtable = (ref Stringmap.empty : hint_db_table)
  
  let searchtable_map name = 
!   Stringmap.find name !searchtable
  let searchtable_add (name,db) = 
!   searchtable := Stringmap.add name db !searchtable
  
  (**************************************************************************)
  (*                       Definition of the summary                        *)
  (**************************************************************************)
  
! let init     () = searchtable := Stringmap.empty
  let freeze   () = !searchtable
  let unfreeze fs = searchtable := fs
  
--- 134,161 ----
  
  end
  
! module Hintdbmap = Gmap
  
! 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 Hintdbmap.empty : hint_db_table)
  
  let searchtable_map name = 
!   Hintdbmap.find name !searchtable
  let searchtable_add (name,db) = 
!   searchtable := Hintdbmap.add name db !searchtable
! let current_db_names () =
!   Hintdbmap.dom !searchtable
  
  (**************************************************************************)
  (*                       Definition of the summary                        *)
  (**************************************************************************)
  
! let init     () = searchtable := Hintdbmap.empty
  let freeze   () = !searchtable
  let unfreeze fs = searchtable := fs
  
***************
*** 498,504 ****
  
  (* 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 valid_dbs = 
      map_succeed 
        (fun (name,db) -> (name,db,Hint_db.map_all c db)) 
--- 502,508 ----
  
  (* Print all hints associated to head c in any database *)
  let fmt_hint_list_for_head c = 
!   let dbs = Hintdbmap.to_list !searchtable in
    let valid_dbs = 
      map_succeed 
        (fun (name,db) -> (name,db,Hint_db.map_all c db)) 
***************
*** 523,529 ****
        | [] -> assert false 
      in
      let hd = head_of_constr_reference hdc in
!     let dbs = stringmap_to_list !searchtable in
      let valid_dbs = 
        if occur_existential cl then 
  	map_succeed 
--- 527,533 ----
        | [] -> assert false 
      in
      let hd = head_of_constr_reference hdc in
!     let dbs = Hintdbmap.to_list !searchtable in
      let valid_dbs = 
        if occur_existential cl then 
  	map_succeed 
***************
*** 568,574 ****
    
  (* displays all the hints of all databases *)
  let print_searchtable () =
!   Stringmap.iter
      (fun name db ->
         msg (str "In the database " ++ str name ++ fnl ());
         print_hint_db db)
--- 572,578 ----
    
  (* displays all the hints of all databases *)
  let print_searchtable () =
!   Hintdbmap.iter
      (fun name db ->
         msg (str "In the database " ++ str name ++ fnl ());
         print_hint_db db)
***************
*** 693,699 ****
    tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl 
      
  let full_trivial gl =
!   let dbnames = stringmap_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
--- 697,703 ----
    tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl 
      
  let full_trivial gl =
!   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,804 ****
  let default_auto = auto !default_search_depth []
  
  let full_auto n gl = 
!   let dbnames = stringmap_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
--- 802,808 ----
  let default_auto = auto !default_search_depth []
  
  let full_auto n gl = 
!   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,917 ****
        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
  
  let superauto n to_add argl  = 
    tclTRY (tclCOMPLETE (search_superauto n to_add argl))
--- 915,921 ----
        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 [Hintdbmap.find "core" !searchtable] db argl g
  
  let superauto n to_add argl  = 
    tclTRY (tclCOMPLETE (search_superauto n to_add argl))
Index: tactics/auto.mli
===================================================================
RCS file: /net/pauillac/constr/ARCHIVE/CONSTR/V7/tactics/auto.mli,v
retrieving revision 1.22.2.2
retrieving revision 1.22.2.3
diff -c -r1.22.2.2 -r1.22.2.3
*** tactics/auto.mli	2005/01/21 16:41:52	1.22.2.2
--- tactics/auto.mli	2006/01/25 22:40:29	1.22.2.3
***************
*** 6,12 ****
  (*         *       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*)
  open Util
--- 6,12 ----
  (*         *       GNU Lesser General Public License Version 2.1        *)
  (************************************************************************)
  
! (*i $Id: auto.mli,v 1.22.2.3 2006/01/25 22:40:29 herbelin Exp $ i*)
  
  (*i*)
  open Util
***************
*** 56,66 ****
      val iter : (constr_label -> stored_data list -> unit) -> t -> unit
    end
  
! type frozen_hint_db_table = Hint_db.t Stringmap.t
  
! type hint_db_table = Hint_db.t Stringmap.t ref
  
  type hint_db_name = string
  
  val add_hints : locality_flag -> hint_db_name list -> hints -> unit
  
--- 56,70 ----
      val iter : (constr_label -> stored_data list -> unit) -> t -> unit
    end
  
! type frozen_hint_db_table
  
! 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
  
Index: tactics/eauto.ml4
===================================================================
RCS file: /net/pauillac/constr/ARCHIVE/CONSTR/V7/tactics/eauto.ml4,v
retrieving revision 1.11.2.1
retrieving revision 1.11.2.2
diff -c -r1.11.2.1 -r1.11.2.2
*** tactics/eauto.ml4	2004/07/16 19:30:52	1.11.2.1
--- tactics/eauto.ml4	2006/01/25 22:40:29	1.11.2.2
***************
*** 8,14 ****
  
  (*i camlp4deps: "parsing/grammar.cma" i*)
  
! (* $Id: eauto.ml4,v 1.11.2.1 2004/07/16 19:30:52 herbelin Exp $ *)
  
  open Pp
  open Util
--- 8,14 ----
  
  (*i camlp4deps: "parsing/grammar.cma" i*)
  
! (* $Id: eauto.ml4,v 1.11.2.2 2006/01/25 22:40:29 herbelin Exp $ *)
  
  open Pp
  open Util
***************
*** 391,406 ****
    let db_list =
      List.map
        (fun x -> 
! 	 try Stringmap.find x !searchtable
  	 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 =  list_subtract dbnames ["v62"] in
!   let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
    let local_db = make_local_hint_db gl in
    tclTRY (e_search_auto debug n db_list) gl
  
--- 391,406 ----
    let db_list =
      List.map
        (fun x -> 
! 	 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 = current_db_names () in
    let dbnames =  list_subtract dbnames ["v62"] 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