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).

3 files changed, 18 insertions, 85 deletions

diff --git a/library/nametab.ml b/library/nametab.ml
index a3b3ca6e74..840cf8e380 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -279,10 +279,10 @@ module ExtRefTab = Make(FullPath)(ExtRefEqual)
 module MPTab = Make(FullPath)(MPEqual)
 
 type ccitab = ExtRefTab.t
-let the_ccitab = ref (ExtRefTab.empty : ccitab)
+let the_ccitab = Summary.ref ~name:"ccitab" (ExtRefTab.empty : ccitab)
 
 type mptab = MPTab.t
-let the_modtypetab = ref (MPTab.empty : mptab)
+let the_modtypetab = Summary.ref ~name:"modtypetab" (MPTab.empty : mptab)
 
 module DirPath' =
 struct
@@ -303,7 +303,7 @@ module DirTab = Make(DirPath')(GlobDir)
 (* If we have a (closed) module M having a submodule N, than N does not
    have the entry in [the_dirtab]. *)
 type dirtab = DirTab.t
-let the_dirtab = ref (DirTab.empty : dirtab)
+let the_dirtab = Summary.ref ~name:"dirtab" (DirTab.empty : dirtab)
 
 type universe_id = DirPath.t * int
 
@@ -314,7 +314,7 @@ struct
 end
 module UnivTab = Make(FullPath)(UnivIdEqual)
 type univtab = UnivTab.t
-let the_univtab = ref (UnivTab.empty : univtab)
+let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab)
 
 (* Reversed name tables ***************************************************)
 
@@ -322,14 +322,14 @@ let the_univtab = ref (UnivTab.empty : univtab)
 module Globrevtab = HMap.Make(ExtRefOrdered)
 
 type globrevtab = full_path Globrevtab.t
-let the_globrevtab = ref (Globrevtab.empty : globrevtab)
+let the_globrevtab = Summary.ref ~name:"globrevtab" (Globrevtab.empty : globrevtab)
 
 
 type mprevtab = DirPath.t MPmap.t
-let the_modrevtab = ref (MPmap.empty : mprevtab)
+let the_modrevtab = Summary.ref ~name:"modrevtab" (MPmap.empty : mprevtab)
 
 type mptrevtab = full_path MPmap.t
-let the_modtyperevtab = ref (MPmap.empty : mptrevtab)
+let the_modtyperevtab = Summary.ref ~name:"modtyperevtab" (MPmap.empty : mptrevtab)
 
 module UnivIdOrdered =
 struct
@@ -344,7 +344,7 @@ end
 module UnivIdMap = HMap.Make(UnivIdOrdered)
 
 type univrevtab = full_path UnivIdMap.t
-let the_univrevtab = ref (UnivIdMap.empty : univrevtab)
+let the_univrevtab = Summary.ref ~name:"univrevtab" (UnivIdMap.empty : univrevtab)
 
 (* Push functions *********************************************************)
 
@@ -546,38 +546,6 @@ let global_inductive qid =
 
 (********************************************************************)
 
-(********************************************************************)
-(* Registration of tables as a global table and rollback            *)
-
-type frozen = ccitab * dirtab * mptab * univtab
-    * globrevtab * mprevtab * mptrevtab * univrevtab
-
-let freeze _ : frozen =
-  !the_ccitab,
-  !the_dirtab,
-  !the_modtypetab,
-  !the_univtab,
-  !the_globrevtab,
-  !the_modrevtab,
-  !the_modtyperevtab,
-  !the_univrevtab
-
-let unfreeze (ccit,dirt,mtyt,univt,globr,modr,mtyr,univr) =
-  the_ccitab := ccit;
-  the_dirtab := dirt;
-  the_modtypetab := mtyt;
-  the_univtab := univt;
-  the_globrevtab := globr;
-  the_modrevtab := modr;
-  the_modtyperevtab := mtyr;
-  the_univrevtab := univr
-
-let _ =
-  Summary.declare_summary "names"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = Summary.nop }
-
 (* Deprecated synonyms *)
 
 let extended_locate = locate_extended
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 94da51626f..b264e31474 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -111,14 +111,18 @@ end
 
 type cl_index = Bijint.Index.t
 
+let init_class_tab =
+  let open Bijint in
+  add CL_FUN { cl_param = 0 } (add CL_SORT { cl_param = 0 } empty)
+
 let class_tab =
-  ref (Bijint.empty : cl_info_typ Bijint.t)
+  Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ Bijint.t)
 
 let coercion_tab =
-  ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
+  Summary.ref ~name:"coercion_tab" (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
 
 let coercions_in_scope =
-  ref GlobRef.Set_env.empty
+  Summary.ref ~name:"coercions_in_scope" GlobRef.Set_env.empty
 
 module ClPairOrd =
 struct
@@ -131,15 +135,7 @@ end
 module ClPairMap = Map.Make(ClPairOrd)
 
 let inheritance_graph =
-  ref (ClPairMap.empty : inheritance_path ClPairMap.t)
-
-let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph, !coercions_in_scope)
-
-let unfreeze (fcl,fco,fig,in_scope) =
-  class_tab:=fcl;
-  coercion_tab:=fco;
-  inheritance_graph:=fig;
-  coercions_in_scope:=in_scope
+  Summary.ref ~name:"inheritance_graph" (ClPairMap.empty : inheritance_path ClPairMap.t)
 
 (* ajout de nouveaux "objets" *)
 
@@ -153,21 +149,6 @@ let add_new_coercion coe s =
 let add_new_path x y =
   inheritance_graph := ClPairMap.add x y !inheritance_graph
 
-let init () =
-  class_tab:= Bijint.empty;
-  add_new_class CL_FUN  { cl_param = 0 };
-  add_new_class CL_SORT { cl_param = 0 };
-  coercion_tab:= CoeTypMap.empty;
-  inheritance_graph:= ClPairMap.empty
-
-let _ =
-  Summary.declare_summary "inh_graph"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
-
-let _ = init()
-
 (* class_info : cl_typ -> int * cl_info_typ *)
 
 let class_info cl = Bijint.revmap cl !class_tab
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            *)
 (**************************************************************************)