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.
---
 tactics/hints.ml  | 7 +------
 tactics/hints.mli | 3 ---
 2 files changed, 1 insertion(+), 9 deletions(-)

(limited to 'tactics')

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


From 448a1dd0763a36eddf52ee2feadf93479d34b347 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 11 Sep 2018 23:44:54 +0200
Subject: Replace trivial uses of declare_summary with summary.refs

The one in notation.ml looks trivial but is needed to do
with_notation_protection (used by inductive/fixpoint local notations).
---
 tactics/hints.ml | 20 ++------------------
 1 file changed, 2 insertions(+), 18 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 5b21cb7218..3835dee299 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -734,8 +734,6 @@ module Hintdbmap = String.Map
 
 type hint_db = Hint_db.t
 
-type hint_db_table = hint_db Hintdbmap.t ref
-
 (** Initially created hint databases, for typeclasses and rewrite *)
 
 let typeclasses_db = "typeclass_instances"
@@ -746,8 +744,8 @@ let auto_init_db =
     (Hintdbmap.add rewrite_db (Hint_db.empty cst_full_transparent_state true)
        Hintdbmap.empty)
 
-let searchtable : hint_db_table = ref auto_init_db
-let statustable = ref KNmap.empty
+let searchtable = Summary.ref ~name:"searchtable" auto_init_db
+let statustable = Summary.ref ~name:"statustable" KNmap.empty
 
 let searchtable_map name =
   Hintdbmap.find name !searchtable
@@ -761,20 +759,6 @@ let current_pure_db () = List.map snd (current_db ())
 let error_no_such_hint_database x =
   user_err ~hdr:"Hints" (str "No such Hint database: " ++ str x ++ str ".")
 
-(**************************************************************************)
-(*                       Definition of the summary                        *)
-(**************************************************************************)
-
-let init     () =
-  searchtable := auto_init_db; statustable := KNmap.empty
-let freeze   _ = (!searchtable, !statustable)
-let unfreeze (fs, st) = searchtable := fs; statustable := st
-
-let _ = Summary.declare_summary "search"
-	  { Summary.freeze_function   = freeze;
-	    Summary.unfreeze_function = unfreeze;
-	    Summary.init_function     = init }
-
 (**************************************************************************)
 (*             Auxiliary functions to prepare AUTOHINT objects            *)
 (**************************************************************************)
-- 
cgit v1.2.3