diff options
| author | Pierre-Marie Pédrot | 2018-09-23 17:22:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-23 17:22:03 +0200 |
| commit | 92fbd7383c3897b3932b0ad95afa0982d2d8a7e3 (patch) | |
| tree | c09d6b23ceb48e76355e21acdc335d998ed9e77e /plugins | |
| parent | 8c15896b3d3cbfc11f5c493282be3dc1c5c27315 (diff) | |
| parent | 448a1dd0763a36eddf52ee2feadf93479d34b347 (diff) | |
Merge PR #8465: Small cleanup of summary uses
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) |