Some cleanup in Auto

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16758 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 20 insertions, 17 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 05037a150f..fa9bfab992 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -690,8 +690,6 @@ let pr_assumptionset env s =
     ] in
     prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
 
-let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m []
-
 open Typeclasses
 
 let pr_instance i =
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 033f460623..afb8121e8c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -460,9 +460,7 @@ let searchtable_map name =
   Hintdbmap.find name !searchtable
 let searchtable_add (name,db) =
   searchtable := Hintdbmap.add name db !searchtable
-let current_db_names () =
-  let fold k _ acc = k :: acc in
-  List.rev (Hintdbmap.fold fold !searchtable [])
+let current_db_names () = Hintdbmap.domain !searchtable
 let current_db () = Hintdbmap.bindings !searchtable
 
 (**************************************************************************)
@@ -1368,9 +1366,9 @@ let trivial ?(debug=Off) lems dbnames gl =
     (trivial_fail_db d false db_list (make_local_hint_db false lems gl)) gl
 
 let full_trivial ?(debug=Off) lems gl =
-  let dbnames = current_db_names () in
-  let dbnames = List.remove "v62" dbnames in
-  let db_list = List.map (fun x -> searchtable_map x) dbnames in
+  let dbs = !searchtable in
+  let dbs = String.Map.remove "v62" dbs in
+  let db_list = List.map snd (String.Map.bindings dbs) in
   let d = mk_trivial_dbg debug in
   tclTRY_dbg d
     (trivial_fail_db d false db_list (make_local_hint_db false lems gl)) gl
@@ -1441,9 +1439,9 @@ let new_auto ?(debug=Off) n = delta_auto ~debug true n
 let default_auto = auto !default_search_depth [] []
 
 let delta_full_auto ?(debug=Off) mod_delta n lems gl =
-  let dbnames = current_db_names () in
-  let dbnames = List.remove "v62" dbnames in
-  let db_list = List.map (fun x -> searchtable_map x) dbnames in
+  let dbs = !searchtable in
+  let dbs = String.Map.remove "v62" dbs in
+  let db_list = List.map snd (String.Map.bindings dbs) in
   let d = mk_auto_dbg debug in
   tclTRY_dbg d
     (search d n mod_delta db_list (make_local_hint_db false lems gl)) gl
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 5a5b8f56c6..b8860f0978 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Names
 open Term
 open Context
@@ -117,7 +118,7 @@ val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit
 
 val remove_hints : bool -> hint_db_name list -> global_reference list -> unit
 
-val current_db_names : unit -> hint_db_name list
+val current_db_names : unit -> String.Set.t
 
 val interp_hints : hints_expr -> hints_entry
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 6b607c38d2..49b7ec710d 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -358,8 +358,8 @@ let eauto ?(debug=Off) np lems dbnames =
 
 let full_eauto ?(debug=Off) n lems gl =
   let dbnames = current_db_names () in
-  let dbnames =  List.remove "v62" dbnames in
-  let db_list = List.map searchtable_map dbnames in
+  let dbnames =  String.Set.remove "v62" dbnames in
+  let db_list = List.map searchtable_map (String.Set.elements dbnames) in
   tclTRY (e_search_auto debug n lems db_list) gl
 
 let gen_eauto ?(debug=Off) np lems = function
@@ -461,12 +461,18 @@ let autounfold db cls gl =
     | OnConcl occs -> tac occs None)
     cls gl
 
+let autounfold_tac db cls gl =
+  let dbs = match db with
+  | None -> String.Set.elements (Auto.current_db_names ())
+  | Some [] -> ["core"]
+  | Some l -> l
+  in
+  autounfold dbs (Extraargs.glob_in_arg_hyp_to_clause cls) gl
+
 open Extraargs
 
 TACTIC EXTEND autounfold
-| [ "autounfold" hintbases(db) in_arg_hyp(id) ] ->
-    [ autounfold (match db with None -> Auto.current_db_names () | Some [] -> ["core"] | Some x -> x) 
-	(glob_in_arg_hyp_to_clause id) ]
+| [ "autounfold" hintbases(db) in_arg_hyp(id) ] -> [ autounfold_tac db id ]
 END
 
 let unfold_head env (ids, csts) c =