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 /plugins | |
| 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.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 5 |
1 files changed, 0 insertions, 5 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) |