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