From 11a748d42dbf8536abceccbedc350806fcdab8eb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 11 Sep 2018 23:17:28 +0200
Subject: Remove Hints.add_hints_init

It was only used in ltac/rewrite which as a plugin is too late to
affect init.
---
 plugins/ltac/rewrite.ml | 5 -----
 tactics/hints.ml        | 7 +------
 tactics/hints.mli       | 3 ---
 3 files changed, 1 insertion(+), 14 deletions(-)

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9f8cd2fc4e..5b8bd6d01a 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -520,11 +520,6 @@ let rewrite_db = "rewrite"
 
 let conv_transparent_state = (Id.Pred.empty, Cpred.full)
 
-let _ = 
-  Hints.add_hints_init
-    (fun () ->
-       Hints.create_hint_db false rewrite_db conv_transparent_state true)
-
 let rewrite_transparent_state () =
   Hints.Hint_db.transparent_state (Hints.searchtable_map rewrite_db)
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index dce1a1bef6..5b21cb7218 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -765,13 +765,8 @@ let error_no_such_hint_database x =
 (*                       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 ()
+  searchtable := auto_init_db; statustable := KNmap.empty
 let freeze   _ = (!searchtable, !statustable)
 let unfreeze (fs, st) = searchtable := fs; statustable := st
 
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]"]
-- 
cgit v1.2.3