diff options
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) |