diff options
| author | Gaëtan Gilbert | 2018-09-11 23:17:28 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-19 13:15:24 +0200 |
| commit | 11a748d42dbf8536abceccbedc350806fcdab8eb (patch) | |
| tree | c890774f2dd6a74ce926d6cc6f8c66a80f0f2f3d | |
| parent | 6d74efabf11768ca1df3a2f3d5a65d25f7f95b01 (diff) | |
Remove Hints.add_hints_init
It was only used in ltac/rewrite which as a plugin is too late to
affect init.
| -rw-r--r-- | plugins/ltac/rewrite.ml | 5 | ||||
| -rw-r--r-- | tactics/hints.ml | 7 | ||||
| -rw-r--r-- | tactics/hints.mli | 3 |
3 files changed, 1 insertions, 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]"] |