diff options
| author | Gaëtan Gilbert | 2018-09-11 23:44:54 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-19 13:15:54 +0200 |
| commit | 448a1dd0763a36eddf52ee2feadf93479d34b347 (patch) | |
| tree | 5f201308585e38592589d2474fd93aa20bc92fea /tactics | |
| parent | 11a748d42dbf8536abceccbedc350806fcdab8eb (diff) | |
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).
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 20 |
1 files changed, 2 insertions, 18 deletions
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 @@ -762,20 +760,6 @@ 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 *) (**************************************************************************) |