2 files changed, 2 insertions, 26 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml
index dce1a1bef6..3835dee299 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -734,8 +734,6 @@ module Hintdbmap = String.Map
 
 type hint_db = Hint_db.t
 
-type hint_db_table = hint_db Hintdbmap.t ref
-
 (** Initially created hint databases, for typeclasses and rewrite *)
 
 let typeclasses_db = "typeclass_instances"
@@ -746,8 +744,8 @@ let auto_init_db =
     (Hintdbmap.add rewrite_db (Hint_db.empty cst_full_transparent_state true)
        Hintdbmap.empty)
 
-let searchtable : hint_db_table = ref auto_init_db
-let statustable = ref KNmap.empty
+let searchtable = Summary.ref ~name:"searchtable" auto_init_db
+let statustable = Summary.ref ~name:"statustable" KNmap.empty
 
 let searchtable_map name =
   Hintdbmap.find name !searchtable
@@ -762,25 +760,6 @@ let error_no_such_hint_database x =
   user_err ~hdr:"Hints" (str "No such Hint database: " ++ str x ++ str ".")
 
 (**************************************************************************)
-(*                       Definition of the summary                        *)
-(**************************************************************************)
-
-let hints_init : (unit -> unit) ref = ref (fun () -> ())
-let add_hints_init f =
-  let init = !hints_init in
-  hints_init := (fun () -> init (); f ())
-
-let init     () =
-  searchtable := auto_init_db; statustable := KNmap.empty; !hints_init ()
-let freeze   _ = (!searchtable, !statustable)
-let unfreeze (fs, st) = searchtable := fs; statustable := st
-
-let _ = Summary.declare_summary "search"
-	  { Summary.freeze_function   = freeze;
-	    Summary.unfreeze_function = unfreeze;
-	    Summary.init_function     = init }
-
-(**************************************************************************)
 (*             Auxiliary functions to prepare AUTOHINT objects            *)
 (**************************************************************************)
 
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 9bf6c175a5..c49ca2094a 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -293,8 +293,5 @@ val pr_hint_db : Hint_db.t -> Pp.t
 [@@ocaml.deprecated "please used pr_hint_db_env"]
 val pr_hint : env -> evar_map -> hint -> Pp.t
 
-(** Hook for changing the initialization of auto *)
-val add_hints_init : (unit -> unit) -> unit
-
 type nonrec hint_info = hint_info
 [@@ocaml.deprecated "Use [Typeclasses.hint_info]"]