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 -----
 1 file changed, 5 deletions(-)

(limited to 'plugins')

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)
 
-- 
cgit v1.2.3