code simplifications concerning Summary

 - Most of the time, the table registered via Summary.declare_summary
   is just a single reference. A new function Summary.ref now allows
   to both declare this ref and register it to summary in one shot.

 - Clarifications concerning the role of [init_function].
   For statically registered tables that don't need a special initializer,
   just do nothing there (see the new Summary.nop function).

 Beware: now that Summary exports a function named "ref", any code that
 do an "open Summary" will probably fail to compile.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16441 85f007b7-540e-0410-9357-904b9bb8a0f7

37 files changed, 171 insertions, 536 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 955ad9a88..4b4b36865 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -23,13 +23,7 @@ open Nameops
 open Misctypes
 (*i*)
 
-let generalizable_table = ref Id.Pred.empty
-
-let _ =
-  Summary.declare_summary "generalizable-ident"
-    { Summary.freeze_function = (fun () -> !generalizable_table);
-      Summary.unfreeze_function = (fun r -> generalizable_table := r);
-      Summary.init_function = (fun () -> generalizable_table := Id.Pred.empty) }
+let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident"
 
 let declare_generalizable_ident table (loc,id) =
   if not (Id.equal id (root_of_id id)) then
diff --git a/interp/notation.ml b/interp/notation.ml
index 37ad387da..81ef06f6f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -16,7 +16,6 @@ open Term
 open Nametab
 open Libnames
 open Globnames
-open Summary
 open Constrexpr
 open Notation_term
 open Glob_term
@@ -920,10 +919,10 @@ let init () =
   scope_class_map := Gmap.add ScopeSort "type_scope" Gmap.empty
 
 let _ =
-  declare_summary "symbols"
-    { freeze_function = freeze;
-      unfreeze_function = unfreeze;
-      init_function = init }
+  Summary.declare_summary "symbols"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init }
 
 let with_notation_protection f x =
   let fs = freeze () in
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 30953007e..0efcafcd2 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -22,8 +22,8 @@ type key =
   | RefKey of global_reference
   | Oth
 
-let reserve_table = ref Id.Map.empty
-let reserve_revtable = ref Gmapl.empty
+let reserve_table = Summary.ref Id.Map.empty ~name:"reserved-type"
+let reserve_revtable = Summary.ref Gmapl.empty ~name:"reserved-type-rev"
 
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
   | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
@@ -41,17 +41,6 @@ let in_reserved : Id.t * notation_constr -> obj =
   declare_object {(default_object "RESERVED-TYPE") with
     cache_function = cache_reserved_type }
 
-let freeze_reserved () = (!reserve_table,!reserve_revtable)
-let unfreeze_reserved (r,rr) = reserve_table := r; reserve_revtable := rr
-let init_reserved () =
-  reserve_table := Id.Map.empty; reserve_revtable := Gmapl.empty
-
-let _ =
-  Summary.declare_summary "reserved-type"
-    { Summary.freeze_function = freeze_reserved;
-      Summary.unfreeze_function = unfreeze_reserved;
-      Summary.init_function = init_reserved }
-
 let declare_reserved_type_binding (loc,id) t =
   if not (Id.equal id (root_of_id id)) then
     user_err_loc(loc,"declare_reserved_type",
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 96ba0bcc5..a023462b7 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -21,13 +21,9 @@ open Nametab
 
 type version = Flags.compat_version option
 
-let syntax_table = ref (KNmap.empty : (interpretation*version) KNmap.t)
-
-let _ = Summary.declare_summary
-	  "SYNTAXCONSTANT"
-	  { Summary.freeze_function = (fun () -> !syntax_table);
-	    Summary.unfreeze_function = (fun ft -> syntax_table := ft);
-	    Summary.init_function = (fun () -> syntax_table := KNmap.empty) }
+let syntax_table =
+  Summary.ref (KNmap.empty : (interpretation*version) KNmap.t)
+    ~name:"SYNTAXCONSTANT"
 
 let add_syntax_constant kn c onlyparse =
   syntax_table := KNmap.add kn (c,onlyparse) !syntax_table
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 6f013e46f..758bf821f 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -28,6 +28,10 @@ type oracle = level Id.Map.t * level Cmap.t
 let var_opacity = ref Id.Map.empty
 let cst_opacity = ref Cmap.empty
 
+(* summary operations *)
+let freeze () = (!var_opacity, !cst_opacity)
+let unfreeze (vo,co) = (cst_opacity := co; var_opacity := vo)
+
 let get_strategy = function
   | VarKey id ->
       (try Id.Map.find id !var_opacity
@@ -65,8 +69,3 @@ let oracle_order l2r k1 k2 =
     | Level n1, Opaque -> true
     | Level n1, Level n2 -> n1 < n2
     | _ -> l2r (* use recommended default *)
-
-(* summary operations *)
-let init() = (cst_opacity := Cmap.empty; var_opacity := Id.Map.empty)
-let freeze () = (!var_opacity, !cst_opacity)
-let unfreeze (vo,co) = (cst_opacity := co; var_opacity := vo)
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 2a6db4b4b..4d8779664 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -36,6 +36,5 @@ val get_transp_state : unit -> transparent_state
 (****************************
    Summary operations *)
 type oracle
-val init     : unit -> unit
 val freeze   : unit -> oracle
 val unfreeze : oracle -> unit
diff --git a/library/declaremods.ml b/library/declaremods.ml
index bdb7bd368..cf333a886 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -83,10 +83,14 @@ type substitutive_objects =
    * Modules which where created with Module M:=mexpr or with
      Module M:SIG. ... End M. have the keep list empty.
 *)
+
 let modtab_substobjs =
-  ref (MPmap.empty : substitutive_objects MPmap.t)
+  Summary.ref (MPmap.empty : substitutive_objects MPmap.t)
+    ~name:"MODULE-INFO-1"
+
 let modtab_objects =
-  ref (MPmap.empty : (object_prefix * lib_objects) MPmap.t)
+  Summary.ref (MPmap.empty : (object_prefix * lib_objects) MPmap.t)
+    ~name:"MODULE-INFO-2"
 
 type current_module_info = {
   cur_mp : module_path; (** current started interactive module (if any) *)
@@ -101,34 +105,12 @@ let default_module_info =
     cur_typ = None;
     cur_typs = [] }
 
-let openmod_info = ref default_module_info
+let openmod_info = Summary.ref default_module_info ~name:"MODULE-INFO-3"
 
 (* The library_cache here is needed to avoid recalculations of
    substituted modules object during "reloading" of libraries *)
-let library_cache = ref Dirmap.empty
-
-let freeze_mod_tables () =
-  !modtab_substobjs,
-  !modtab_objects,
-  !openmod_info,
-  !library_cache
-
-let unfreeze_mod_tables (sobjs,objs,info,libcache) =
-  modtab_substobjs := sobjs;
-  modtab_objects := objs;
-  openmod_info := info;
-  library_cache := libcache
-
-let init_mod_tables () =
-  modtab_substobjs := MPmap.empty;
-  modtab_objects := MPmap.empty;
-  openmod_info := default_module_info;
-  library_cache := Dirmap.empty
-
-let _ = Summary.declare_summary "MODULE-INFO"
-  { Summary.freeze_function = freeze_mod_tables;
-    Summary.unfreeze_function = unfreeze_mod_tables;
-    Summary.init_function = init_mod_tables }
+let library_cache = Summary.ref Dirmap.empty ~name:"MODULE-INFO-4"
+
 
 (* auxiliary functions to transform full_path and kernel_name given
    by Lib into module_path and DirPath.t needed for modules *)
@@ -303,24 +285,14 @@ let in_modkeep : lib_objects -> obj =
    The module M gets its objects from SIG
 *)
 let modtypetab =
-  ref (MPmap.empty : substitutive_objects MPmap.t)
+  Summary.ref (MPmap.empty : substitutive_objects MPmap.t)
+    ~name:"MODTYPE-INFO-1"
 
 (* currently started interactive module type. We remember its arguments
    if it is a functor type *)
 let openmodtype_info =
-  ref ([],[] : MBId.t list * module_type_body list)
-
-let freeze_modtyp_tables () =
-  !modtypetab, !openmodtype_info
-let unfreeze_modtyp_tables (mtt,omti) =
-  modtypetab := mtt; openmodtype_info := omti
-let init_modtyp_tables () =
-  modtypetab := MPmap.empty; openmodtype_info := [],[]
-
-let _ = Summary.declare_summary "MODTYPE-INFO"
-  { Summary.freeze_function = freeze_modtyp_tables;
-    Summary.unfreeze_function = unfreeze_modtyp_tables;
-    Summary.init_function = init_modtyp_tables }
+  Summary.ref ([],[] : MBId.t list * module_type_body list)
+    ~name:"MODTYPE-INFO-2"
 
 let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) =
   let mp = mp_of_kn kn in
diff --git a/library/decls.ml b/library/decls.ml
index 0ceea8b43..a93913a77 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -20,12 +20,8 @@ open Libnames
 type variable_data =
     DirPath.t * bool (* opacity *) * Univ.constraints * logical_kind
 
-let vartab = ref (Id.Map.empty : variable_data Id.Map.t)
-
-let _ = Summary.declare_summary "VARIABLE"
-  { Summary.freeze_function = (fun () -> !vartab);
-    Summary.unfreeze_function = (fun ft -> vartab := ft);
-    Summary.init_function = (fun () -> vartab := Id.Map.empty) }
+let vartab =
+  Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE"
 
 let add_variable_data id o = vartab := Id.Map.add id o !vartab
 
@@ -42,12 +38,7 @@ let variable_exists id = Id.Map.mem id !vartab
 
 (** Datas associated to global parameters and constants *)
 
-let csttab = ref (Cmap.empty : logical_kind Cmap.t)
-
-let _ = Summary.declare_summary "CONSTANT"
-	  { Summary.freeze_function = (fun () -> !csttab);
-	    Summary.unfreeze_function = (fun ft -> csttab := ft);
-	    Summary.init_function = (fun () -> csttab := Cmap.empty) }
+let csttab = Summary.ref (Cmap.empty : logical_kind Cmap.t) ~name:"CONSTANT"
 
 let add_constant_kind kn k = csttab := Cmap.add kn k !csttab
 
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index c26f652df..64267db01 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -10,28 +10,10 @@ open Libnames
 
 type discharged_hyps = full_path list
 
-let discharged_hyps_map = ref Spmap.empty
+let discharged_hyps_map = Summary.ref Spmap.empty ~name:"discharged_hypothesis"
 
 let set_discharged_hyps sp hyps =
   discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
 
 let get_discharged_hyps sp =
-  try
-   Spmap.find sp !discharged_hyps_map
-  with Not_found ->
-    []
-
-(*s Registration as global tables and rollback. *)
-
-let init () =
-  discharged_hyps_map := Spmap.empty
-
-let freeze () = !discharged_hyps_map
-
-let unfreeze dhm = discharged_hyps_map := dhm
-
-let _ =
-  Summary.declare_summary "discharged_hypothesis"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+  try Spmap.find sp !discharged_hyps_map with Not_found -> []
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli
index bc90220db..f2173bf49 100644
--- a/library/dischargedhypsmap.mli
+++ b/library/dischargedhypsmap.mli
@@ -13,8 +13,8 @@ open Nametab
 
 type discharged_hyps = full_path list
 
-(** Discharged hypothesis. Here we store the discharged hypothesis of each 
-    constant or inductive type declaration.                                *)
+(** Discharged hypothesis. Here we store the discharged hypothesis of each
+    constant or inductive type declaration. *)
 
 val set_discharged_hyps : full_path -> discharged_hyps -> unit
 val get_discharged_hyps : full_path -> discharged_hyps
diff --git a/library/global.ml b/library/global.ml
index 929f7418f..f120ef195 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -10,12 +10,11 @@ open Names
 open Term
 open Environ
 open Safe_typing
-open Summary
 
 (* We introduce here the global environment of the system, and we declare it
    as a synchronized table. *)
 
-let global_env = ref empty_environment
+let global_env = Summary.ref empty_environment ~name:"Global environment"
 
 let safe_env () = !global_env
 
@@ -23,12 +22,6 @@ let env () = env_of_safe_env !global_env
 
 let env_is_empty () = is_empty !global_env
 
-let _ =
-  declare_summary "Global environment"
-    { freeze_function = (fun () -> !global_env);
-      unfreeze_function = (fun fr -> global_env := fr);
-      init_function = (fun () -> global_env := empty_environment) }
-
 (* Then we export the functions of [Typing] on that environment. *)
 
 let universes () = universes (env())
diff --git a/library/goptions.ml b/library/goptions.ml
index 381b67726..bdc6ab89d 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -65,17 +65,10 @@ module MakeTable =
 
     module MySet = Set.Make (struct type t = A.t let compare = compare end)
 
-    let t = ref (MySet.empty : MySet.t)
-
-    let _ =
-      if A.synchronous then
-	let freeze () = !t in
-	let unfreeze c = t := c in
-	let init () = t := MySet.empty in
-	Summary.declare_summary nick
-          { Summary.freeze_function = freeze;
-            Summary.unfreeze_function = unfreeze;
-            Summary.init_function = init }
+    let t =
+      if A.synchronous
+      then Summary.ref MySet.empty ~name:nick
+      else ref MySet.empty
 
     let (add_option,remove_option) =
       if A.synchronous then
@@ -216,7 +209,6 @@ with Not_found ->
     or List.mem_assoc (nickname key) !ref_table
   then error "Sorry, this option name is already used."
 
-open Summary
 open Libobject
 open Lib
 
@@ -247,10 +239,10 @@ let declare_option cast uncast
 		       discharge_function = (fun (_,v) -> Some v);
 		       load_function = (fun _ (_,v) -> write v)}
     in
-    let _ = declare_summary (nickname key)
-	     { freeze_function = read;
-	       unfreeze_function = write;
-	       init_function = (fun () -> write default) }
+    let _ = Summary.declare_summary (nickname key)
+	     { Summary.freeze_function = read;
+	       Summary.unfreeze_function = write;
+	       Summary.init_function = (fun () -> write default) }
     in
     begin fun v -> add_anonymous_leaf (decl_obj v) end ,
     begin fun v -> add_anonymous_leaf (ldecl_obj v) end ,
diff --git a/library/heads.ml b/library/heads.ml
index e6c9bc9a8..022e61156 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -52,19 +52,7 @@ module Evalrefmap =
   Map.Make (Evalreford)
 
 
-let head_map = ref Evalrefmap.empty
-
-let init () = head_map := Evalrefmap.empty
-
-let freeze () = !head_map
-
-let unfreeze hm = head_map := hm
-
-let _ =
-  Summary.declare_summary "Head_decl"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+let head_map = Summary.ref Evalrefmap.empty ~name:"Head_decl"
 
 let variable_head id  = Evalrefmap.find (EvalVarRef id) !head_map
 let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map
diff --git a/library/impargs.ml b/library/impargs.ml
index 56dca8e3f..0026bc489 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -463,7 +463,7 @@ type implicit_discharge_request =
   | ImplInteractive of global_reference * implicits_flags *
       implicit_interactive_request
 
-let implicits_table = ref Refmap.empty
+let implicits_table = Summary.ref Refmap.empty ~name:"implicits"
 
 let implicits_of_global ref =
   try
@@ -713,15 +713,3 @@ let rec select_impargs_size n = function
 let select_stronger_impargs = function
   | [] -> [] (* Tolerance for (DefaultImpArgs,[]) *)
   | (_,impls)::_ -> impls
-
-(*s Registration as global tables *)
-
-let init () = implicits_table := Refmap.empty
-let freeze () = !implicits_table
-let unfreeze t = implicits_table := t
-
-let _ =
-  Summary.declare_summary "implicits"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
diff --git a/library/lib.ml b/library/lib.ml
index 30beb653f..c7454edaf 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -13,7 +13,6 @@ open Libnames
 open Globnames
 open Nameops
 open Libobject
-open Summary
 
 type is_type = bool (* Module Type or just Module *)
 type export = bool option (* None for a Module Type *)
@@ -217,10 +216,7 @@ let anonymous_id =
   fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n))
 
 let add_anonymous_entry node =
-  let id = anonymous_id () in
-  let name = make_oname id in
-  add_entry name node;
-  name
+  add_entry (make_oname (anonymous_id ())) node
 
 let add_leaf id obj =
   let (path, _) = current_prefix () in
@@ -253,7 +249,7 @@ let add_anonymous_leaf obj =
   add_entry oname (Leaf obj)
 
 let add_frozen_state () =
-  let _ = add_anonymous_entry (FrozenState (freeze_summaries())) in ()
+  add_anonymous_entry (FrozenState (Summary.freeze_summaries()))
 
 (* Modules. *)
 
@@ -331,7 +327,7 @@ let start_compilation s mp =
   if not (Names.DirPath.equal (snd (snd (!path_prefix))) Names.DirPath.empty) then
     error "some sections are already opened";
   let prefix = s, (mp, Names.DirPath.empty) in
-  let _ = add_anonymous_entry (CompilingLibrary prefix) in
+  let () = add_anonymous_entry (CompilingLibrary prefix) in
   comp_name := Some s;
   path_prefix := prefix
 
@@ -406,8 +402,9 @@ type variable_context = variable_info list
 type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap.t
 
 let sectab =
-  ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list *
-		Cooking.work_list * abstr_list) list)
+  Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list *
+		        Cooking.work_list * abstr_list) list)
+    ~name:"section-context"
 
 let add_section () =
   sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),(Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
@@ -475,16 +472,6 @@ let section_instance = function
 let is_in_section ref =
   try ignore (section_instance ref); true with Not_found -> false
 
-let init_sectab () = sectab := []
-let freeze_sectab () = !sectab
-let unfreeze_sectab s = sectab := s
-
-let _ =
-  Summary.declare_summary "section-context"
-    { Summary.freeze_function = freeze_sectab;
-      Summary.unfreeze_function = unfreeze_sectab;
-      Summary.init_function = init_sectab }
-
 (*************)
 (* Sections. *)
 
@@ -502,7 +489,7 @@ let open_section id =
   let name = make_path id, make_kn id (* this makes little sense however *) in
   if Nametab.exists_section dir then
     errorlabstrm "open_section" (pr_id id ++ str " already exists.");
-  let fs = freeze_summaries() in
+  let fs = Summary.freeze_summaries() in
   add_entry name (OpenedSection (prefix, fs));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
@@ -564,7 +551,7 @@ let set_lib_stk new_lib_stk =
   lib_stk := new_lib_stk;
   recalc_path_prefix ();
   let spf = match find_entry_p is_frozen_state with
-    | (sp, FrozenState f) -> unfreeze_summaries f; sp
+    | (sp, FrozenState f) -> Summary.unfreeze_summaries f; sp
     | _ -> assert false
   in
   let (after,_,_) = split_lib spf in
@@ -635,7 +622,7 @@ let init () =
   add_frozen_state ();
   comp_name := None;
   path_prefix := initial_prefix;
-  init_summaries()
+  Summary.init_summaries ()
 
 (* Misc *)
 
diff --git a/library/library.ml b/library/library.ml
index 7c34a62d0..e1ef4515d 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -45,40 +45,16 @@ module LibraryMap = Map.Make(LibraryOrdered)
 module LibraryFilenameMap = Map.Make(LibraryOrdered)
 
 (* This is a map from names to loaded libraries *)
-let libraries_table = ref LibraryMap.empty
+let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY"
 
 (* This is the map of loaded libraries filename *)
 (* (not synchronized so as not to be caught in the states on disk) *)
 let libraries_filename_table = ref LibraryFilenameMap.empty
 
 (* These are the _ordered_ sets of loaded, imported and exported libraries *)
-let libraries_loaded_list = ref []
-let libraries_imports_list = ref []
-let libraries_exports_list = ref []
-
-let freeze () =
-  !libraries_table,
-  !libraries_loaded_list,
-  !libraries_imports_list,
-  !libraries_exports_list
-
-let unfreeze (mt,mo,mi,me) =
-  libraries_table := mt;
-  libraries_loaded_list := mo;
-  libraries_imports_list := mi;
-  libraries_exports_list := me
-
-let init () =
-  libraries_table := LibraryMap.empty;
-  libraries_loaded_list := [];
-  libraries_imports_list := [];
-  libraries_exports_list := []
-
-let _ =
-  Summary.declare_summary "MODULES"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD"
+let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT"
+let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT"
 
 (* various requests to the tables *)
 
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 315cbf96e..873703aff 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -20,13 +20,7 @@ type t = {
   path_is_root : bool;
 }
 
-let load_paths = ref ([] : t list)
-
-let () = Summary.declare_summary "LOADPATHS" {
-  Summary.freeze_function = (fun () -> !load_paths);
-  Summary.unfreeze_function = (fun l -> load_paths := l);
-  Summary.init_function = (fun () -> load_paths := []);
-}
+let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS"
 
 let logical p = p.path_logical
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 01324a3a4..1d43725f6 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -540,19 +540,9 @@ let global_inductive r =
 (********************************************************************)
 (* Registration of tables as a global table and rollback            *)
 
-type frozen = ccitab * dirtab * mptab * kntab 
+type frozen = ccitab * dirtab * mptab * kntab
     * globrevtab * mprevtab * mptrevtab * knrevtab
 
-let init () =
-  the_ccitab := ExtRefTab.empty;
-  the_dirtab := DirTab.empty;
-  the_modtypetab := MPTab.empty;
-  the_tactictab := KnTab.empty;
-  the_globrevtab := Globrevtab.empty;
-  the_modrevtab := MPmap.empty;
-  the_modtyperevtab := MPmap.empty;
-  the_tacticrevtab := KNmap.empty
-
 let freeze () : frozen =
   !the_ccitab,
   !the_dirtab,
@@ -577,7 +567,7 @@ let _ =
   Summary.declare_summary "names"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+      Summary.init_function = Summary.nop }
 
 (* Deprecated synonyms *)
 
diff --git a/library/summary.ml b/library/summary.ml
index c6de35744..797cb64bf 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -19,6 +19,9 @@ let summaries =
   (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t)
 
 let internal_declare_summary sumname sdecl =
+  if Hashtbl.mem summaries sumname then
+    anomaly ~label:"Summary.declare_summary"
+      (str "Cannot declare a summary twice: " ++ str sumname);
   let (infun,outfun) = Dyn.create sumname in
   let dyn_freeze () = infun (sdecl.freeze_function())
   and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
@@ -28,9 +31,6 @@ let internal_declare_summary sumname sdecl =
     unfreeze_function = dyn_unfreeze;
     init_function = dyn_init }
   in
-  if Hashtbl.mem summaries sumname then
-    anomaly ~label:"Summary.declare_summary"
-      (str "Cannot declare a summary twice: " ++ str sumname);
   Hashtbl.add summaries sumname ddecl
 
 let declare_summary sumname decl =
@@ -45,7 +45,6 @@ let freeze_summaries () =
     summaries;
   !m
 
-
 let unfreeze_summaries fs =
   Hashtbl.iter
     (fun id decl ->
@@ -55,3 +54,18 @@ let unfreeze_summaries fs =
 
 let init_summaries () =
   Hashtbl.iter (fun _ decl -> decl.init_function()) summaries
+
+(** For global tables registered statically before the end of coqtop
+    launch, the following empty [init_function] could be used. *)
+
+let nop () = ()
+
+(** All-in-one reference declaration + registration *)
+
+let ref ~name x =
+  let r = ref x in
+  declare_summary name
+    { freeze_function = (fun () -> !r);
+      unfreeze_function = ((:=) r);
+      init_function = (fun () -> r := x) };
+  r
diff --git a/library/summary.mli b/library/summary.mli
index 7ded099ab..fd1b324c9 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -14,17 +14,36 @@ type 'a summary_declaration = {
   unfreeze_function : 'a -> unit;
   init_function : unit -> unit }
 
+(** For tables registered during the launch of coqtop, the [init_function]
+    will be run only once, during an [init_summaries] done at the end of
+    coqtop initialization. For tables registered later (for instance
+    during a plugin dynlink), [init_function] is used when unfreezing
+    an earlier frozen state that doesn't contain any value for this table.
+
+    Beware: for tables registered dynamically after the initialization
+    of Coq, their init functions may not be run immediately. It is hence
+    the responsability of plugins to initialize themselves properly.
+*)
+
 val declare_summary : string -> 'a summary_declaration -> unit
 
+(** All-in-one reference declaration + summary registration.
+    It behaves just as OCaml's standard [ref] function, except
+    that a [declare_summary] is done, with [name] as string.
+    The [init_function] restores the reference to its initial value. *)
+
+val ref : name:string -> 'a -> 'a ref
+
+(** For global tables registered statically before the end of coqtop
+    launch, the following empty [init_function] could be used. *)
+
+val nop : unit -> unit
+
+(** The type [frozen] is a snapshot of the states of all the registered
+    tables of the system. *)
+
 type frozen
 
 val freeze_summaries : unit -> frozen
 val unfreeze_summaries : frozen -> unit
 val init_summaries : unit -> unit
-
-(** Beware: if some code is dynamically loaded via dynlink after the
-    initialization of Coq, the init functions of any summary declared
-    by this code may not be run. It is hence the responsability of
-    plugins to initialize themselves properly.
-*)
-
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 8edc56467..85e80dcb6 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -330,13 +330,11 @@ let init_grammar () =
 let init () =
   init_grammar ()
 
-open Summary
-
 let _ =
-  declare_summary "GRAMMAR_LEXER"
-    { freeze_function = freeze;
-      unfreeze_function = unfreeze;
-      init_function = init }
+  Summary.declare_summary "GRAMMAR_LEXER"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init }
 
 let with_grammar_rule_protection f x =
   let fs = freeze () in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a848d9c21..ebe7230ec 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -11,7 +11,6 @@ open Term
 open Declarations
 open Nameops
 open Namegen
-open Summary
 open Libobject
 open Goptions
 open Libnames
@@ -561,7 +560,7 @@ let _ = declare_string_option
 
 type lang = Ocaml | Haskell | Scheme
 
-let lang_ref = ref Ocaml
+let lang_ref = Summary.ref Ocaml ~name:"ExtrLang"
 
 let lang () = !lang_ref
 
@@ -571,18 +570,13 @@ let extr_lang : lang -> obj =
        cache_function = (fun (_,l) -> lang_ref := l);
        load_function = (fun _ (_,l) -> lang_ref := l)}
 
-let _ = declare_summary "Extraction Lang"
-	  { freeze_function = (fun () -> !lang_ref);
-	    unfreeze_function = ((:=) lang_ref);
-	    init_function = (fun () -> lang_ref := Ocaml) }
-
 let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
 
 (*s Extraction Inline/NoInline *)
 
 let empty_inline_table = (Refset'.empty,Refset'.empty)
 
-let inline_table = ref empty_inline_table
+let inline_table = Summary.ref empty_inline_table ~name:"ExtrInline"
 
 let to_inline r = Refset'.mem r (fst !inline_table)
 
@@ -609,11 +603,6 @@ let inline_extraction : bool * global_reference list -> obj =
         (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
     }
 
-let _ = declare_summary "Extraction Inline"
-	  { freeze_function = (fun () -> !inline_table);
-	    unfreeze_function = ((:=) inline_table);
-	    init_function = (fun () -> inline_table := empty_inline_table) }
-
 (* Grammar entries. *)
 
 let extraction_inline b l =
@@ -652,7 +641,7 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
 type int_or_id = ArgInt of int | ArgId of Id.t
 
-let implicits_table = ref Refmap'.empty
+let implicits_table = Summary.ref Refmap'.empty ~name:"ExtrImplicit"
 
 let implicits_of_global r =
  try Refmap'.find r !implicits_table with Not_found -> []
@@ -688,11 +677,6 @@ let implicit_extraction : global_reference * int_or_id list -> obj =
        subst_function = (fun (s,(r,l)) -> (fst (subst_global s r), l))
     }
 
-let _ = declare_summary "Extraction Implicit"
-	  { freeze_function = (fun () -> !implicits_table);
-	    unfreeze_function = ((:=) implicits_table);
-	    init_function = (fun () -> implicits_table := Refmap'.empty) }
-
 (* Grammar entries. *)
 
 let extraction_implicit r l =
@@ -702,7 +686,7 @@ let extraction_implicit r l =
 
 (*s Extraction Blacklist of filenames not to use while extracting *)
 
-let blacklist_table = ref Id.Set.empty
+let blacklist_table = Summary.ref Id.Set.empty ~name:"ExtrBlacklist"
 
 let modfile_ids = ref []
 let modfile_mps = ref MPmap.empty
@@ -747,11 +731,6 @@ let blacklist_extraction : string list -> obj =
        subst_function = (fun (_,x) -> x)
     }
 
-let _ = declare_summary "Extraction Blacklist"
-	  { freeze_function = (fun () -> !blacklist_table);
-	    unfreeze_function = ((:=) blacklist_table);
-	    init_function = (fun () -> blacklist_table := Id.Set.empty) }
-
 (* Grammar entries. *)
 
 let extraction_blacklist l =
@@ -779,7 +758,7 @@ let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
 let use_type_scheme_nb_args, register_type_scheme_nb_args =
   let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r
 
-let customs = ref Refmap'.empty
+let customs = Summary.ref Refmap'.empty ~name:"ExtrCustom"
 
 let add_custom r ids s = customs := Refmap'.add r (ids,s) !customs
 
@@ -791,7 +770,7 @@ let find_custom r = snd (Refmap'.find r !customs)
 
 let find_type_custom r = Refmap'.find r !customs
 
-let custom_matchs = ref Refmap'.empty
+let custom_matchs = Summary.ref Refmap'.empty ~name:"ExtrCustomMatchs"
 
 let add_custom_match r s =
   custom_matchs := Refmap'.add r s !custom_matchs
@@ -823,11 +802,6 @@ let in_customs : global_reference * string list * string -> obj =
         (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
     }
 
-let _ = declare_summary "ML extractions"
-	  { freeze_function = (fun () -> !customs);
-	    unfreeze_function = ((:=) customs);
-	    init_function = (fun () -> customs := Refmap'.empty) }
-
 let in_custom_matchs : global_reference * string -> obj =
   declare_object
     {(default_object "ML extractions custom matchs") with
@@ -837,11 +811,6 @@ let in_custom_matchs : global_reference * string -> obj =
        subst_function = (fun (subs,(r,s)) -> (fst (subst_global subs r), s))
     }
 
-let _ = declare_summary "ML extractions custom match"
-	  { freeze_function = (fun () -> !custom_matchs);
-	    unfreeze_function = ((:=) custom_matchs);
-	    init_function = (fun () -> custom_matchs := Refmap'.empty) }
-
 (* Grammar entries. *)
 
 let extract_constant_inline inline r ids s =
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 1e8f4afdf..c6f04027b 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -238,8 +238,9 @@ type function_info =
 (* let function_table = ref ([] : function_db) *)
 
 
-let from_function = ref Cmap.empty
-let from_graph = ref Indmap.empty
+let from_function = Summary.ref Cmap.empty ~name:"functions_db_fn"
+let from_graph = Summary.ref Indmap.empty ~name:"functions_db_gr"
+
 (*
 let rec do_cache_info finfo = function
   | [] -> raise Not_found
@@ -371,26 +372,6 @@ let in_Function : function_info -> Libobject.obj =
     }
 
 
-
-(* Synchronisation with reset *)
-let freeze () =
-  !from_function,!from_graph
-let unfreeze (functions,graphs) =
-(*   Pp.msgnl (str "unfreezing function_table : " ++ pr_table l); *)
-  from_function := functions;
-  from_graph := graphs
-
-let init () =
-(*   Pp.msgnl (str "reseting function_table");  *)
-  from_function := Cmap.empty;
-  from_graph := Indmap.empty
-
-let _ =
-  Summary.declare_summary "functions_db_sum"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
-
 let find_or_none id =
   try Some
     (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly (Pp.str "Not a constant")
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 1b2ba0e87..48741525d 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -333,9 +333,9 @@ type ring_info =
 
 module Cmap = Map.Make(struct type t = constr let compare = constr_ord end)
 
-let from_carrier = ref Cmap.empty
-let from_relation = ref Cmap.empty
-let from_name = ref Spmap.empty
+let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
+let from_relation = Summary.ref Cmap.empty ~name:"ring-tac-rel-table"
+let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table"
 
 let ring_for_carrier r = Cmap.find r !from_carrier
 let ring_for_relation rel = Cmap.find rel !from_relation
@@ -366,18 +366,6 @@ let find_ring_structure env sigma l =
             (str"cannot find a declared ring structure for equality"++
              spc()++str"\""++pr_constr req++str"\"")) *)
 
-let _ =
-  Summary.declare_summary "tactic-new-ring-table"
-    { Summary.freeze_function =
-        (fun () -> !from_carrier,!from_relation,!from_name);
-      Summary.unfreeze_function =
-        (fun (ct,rt,nt) ->
-          from_carrier := ct; from_relation := rt; from_name := nt);
-      Summary.init_function =
-        (fun () ->
-          from_carrier := Cmap.empty; from_relation := Cmap.empty;
-          from_name := Spmap.empty) }
-
 let add_entry (sp,_kn) e =
 (*  let _ = ty e.ring_lemma1 in
   let _ = ty e.ring_lemma2 in
@@ -910,10 +898,9 @@ type field_info =
       field_pre_tac : glob_tactic_expr;
       field_post_tac : glob_tactic_expr }
 
-let field_from_carrier = ref Cmap.empty
-let field_from_relation = ref Cmap.empty
-let field_from_name = ref Spmap.empty
-
+let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table"
+let field_from_relation = Summary.ref Cmap.empty ~name:"field-tac-rel-table"
+let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table"
 
 let field_for_carrier r = Cmap.find r !field_from_carrier
 let field_for_relation rel = Cmap.find rel !field_from_relation
@@ -943,19 +930,6 @@ let find_field_structure env sigma l =
             (str"cannot find a declared field structure for equality"++
              spc()++str"\""++pr_constr req++str"\"")) *)
 
-let _ =
-  Summary.declare_summary "tactic-new-field-table"
-    { Summary.freeze_function =
-        (fun () -> !field_from_carrier,!field_from_relation,!field_from_name);
-      Summary.unfreeze_function =
-        (fun (ct,rt,nt) ->
-          field_from_carrier := ct; field_from_relation := rt;
-          field_from_name := nt);
-      Summary.init_function =
-        (fun () ->
-          field_from_carrier := Cmap.empty; field_from_relation := Cmap.empty;
-          field_from_name := Spmap.empty) }
-
 let add_field_entry (sp,_kn) e =
 (*
   let _ = ty e.field_ok in
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 42099f5db..4562c5aa5 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -15,14 +15,9 @@ open Util
 open Libobject
 (*i*)
 
-let empty_name_table = (Refmap.empty : Name.t list list Refmap.t)
-let name_table = ref empty_name_table
-
-let _ =
-  Summary.declare_summary "rename-arguments"
-    { Summary.freeze_function = (fun () -> !name_table);
-      Summary.unfreeze_function = (fun r -> name_table := r);
-      Summary.init_function = (fun () -> name_table := empty_name_table) }
+let name_table =
+  Summary.ref (Refmap.empty : Name.t list list Refmap.t)
+    ~name:"rename-arguments"
 
 type req =
   | ReqLocal
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d9a22b3e7..82dda8e0f 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -164,11 +164,7 @@ let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
 
 (* Generator of metavariables *)
 let new_meta =
-  let meta_ctr = ref 0 in
-  Summary.declare_summary "meta counter"
-    { Summary.freeze_function = (fun () -> !meta_ctr);
-      Summary.unfreeze_function = (fun n -> meta_ctr := n);
-      Summary.init_function = (fun () -> meta_ctr := 0) };
+  let meta_ctr = Summary.ref 0 ~name:"meta counter" in
   fun () -> incr meta_ctr; !meta_ctr
 
 let mk_new_meta () = mkMeta(new_meta())
@@ -262,11 +258,7 @@ let make_pure_subst evi args =
 
 (* Generator of existential names *)
 let new_untyped_evar =
-  let evar_ctr = ref 0 in
-  Summary.declare_summary "evar counter"
-    { Summary.freeze_function = (fun () -> !evar_ctr);
-      Summary.unfreeze_function = (fun n -> evar_ctr := n);
-      Summary.init_function = (fun () -> evar_ctr := 0) };
+  let evar_ctr = Summary.ref 0 ~name:"evar counter" in
   fun () -> incr evar_ctr; existential_of_int !evar_ctr
 
 (*------------------------------------*
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 7c2ac1a27..5aced6e10 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -39,8 +39,10 @@ type struc_typ = {
   s_PROJKIND : (Name.t * bool) list;
   s_PROJ : constant option list }
 
-let structure_table = ref (Indmap.empty : struc_typ Indmap.t)
-let projection_table = ref Cmap.empty
+let structure_table =
+  Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs"
+let projection_table =
+  Summary.ref Cmap.empty ~name:"record-projs"
 
 (* TODO: could be unify struc_typ and struc_tuple ? in particular,
    is the inductive always (fst constructor) ? It seems so... *)
@@ -126,15 +128,7 @@ module MethodsDnet : Term_dnet.S
      let direction = true
    end)
 
-let meth_dnet = ref MethodsDnet.empty
-
-open Summary
-
-let _ =
-  declare_summary "record-methods-state"
-    { freeze_function = (fun () -> !meth_dnet);
-      unfreeze_function = (fun m -> meth_dnet := m);
-      init_function = (fun () -> meth_dnet := MethodsDnet.empty) }
+let meth_dnet = Summary.ref MethodsDnet.empty ~name:"record-methods-state"
 
 open Libobject
 
@@ -194,7 +188,9 @@ type cs_pattern =
   | Sort_cs of sorts_family
   | Default_cs
 
-let object_table = ref (Refmap.empty : (cs_pattern * obj_typ) list Refmap.t)
+let object_table =
+  Summary.ref (Refmap.empty : (cs_pattern * obj_typ) list Refmap.t)
+    ~name:"record-canonical-structs"
 
 let canonical_projections () =
   Refmap.fold (fun x -> List.fold_right (fun (y,c) acc -> ((x,y),c)::acc))
@@ -346,21 +342,3 @@ let is_open_canonical_projection env sigma (c,args) =
       not (isConstruct hd) 
     with Failure _ -> false
   with Not_found -> false
-
-let freeze () =
-  !structure_table, !projection_table, !object_table
-
-let unfreeze (s,p,o) =
-  structure_table := s; projection_table := p; object_table := o
-
-let init () =
-  structure_table := Indmap.empty; projection_table := Cmap.empty;
-  object_table := Refmap.empty
-
-let _ = init()
-
-let _ =
-  Summary.declare_summary "objdefs"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b46b69c62..efc2a7467 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -134,22 +134,7 @@ type constant_evaluation =
 
 type frozen = constant_evaluation Cmap.t
 
-let eval_table = ref (Cmap.empty : frozen)
-
-let init () =
-  eval_table := Cmap.empty
-
-let freeze () =
-  !eval_table
-
-let unfreeze ct =
-  eval_table := ct
-
-let _ =
-  Summary.declare_summary "evaluation"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+let eval_table = Summary.ref (Cmap.empty : frozen) ~name:"evaluation"
 
 (* [compute_consteval] determines whether c is an "elimination constant"
 
@@ -548,13 +533,8 @@ type behaviour = {
   b_dont_expose_case: bool;
 }
 
-let behaviour_table = ref (Refmap.empty : behaviour Refmap.t)
-
-let _ =
-  Summary.declare_summary "simplbehaviour"
-    { Summary.freeze_function = (fun () -> !behaviour_table);
-      Summary.unfreeze_function = (fun x -> behaviour_table := x);
-      Summary.init_function = (fun () -> behaviour_table := Refmap.empty) }
+let behaviour_table =
+  Summary.ref (Refmap.empty : behaviour Refmap.t) ~name:"simplbehaviour"
 
 type simpl_flag = [ `SimplDontExposeCase | `SimplNeverUnfold ]
 type req =
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 25109ffcf..86ff2a28f 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -93,25 +93,8 @@ let new_instance cl pri glob impl =
  * states management
  *)
 
-let classes : typeclasses ref = ref Gmap.empty
-
-let instances : instances ref = ref Gmap.empty
-
-let freeze () = !classes, !instances
-
-let unfreeze (cl,is) =
-  classes:=cl;
-  instances:=is
-
-let init () =
-  classes:= Gmap.empty;
-  instances:= Gmap.empty
-
-let _ =
-  Summary.declare_summary "classes_and_instances"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+let classes : typeclasses ref = Summary.ref Gmap.empty ~name:"classes"
+let instances : instances ref = Summary.ref Gmap.empty ~name:"instances"
 
 let class_info c =
   try Gmap.find c !classes
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 828da8688..80d0ead96 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -20,7 +20,6 @@ open Tacred
 open Closure
 open RedFlags
 open Libobject
-open Summary
 open Misctypes
 
 (* call by value normalisation function using the virtual machine *)
@@ -106,10 +105,10 @@ let inStrategy : strategy_obj -> obj =
 let set_strategy local str =
   Lib.add_anonymous_leaf (inStrategy (local,str))
 
-let _ = declare_summary "Transparent constants and variables"
-    { freeze_function = Conv_oracle.freeze;
-      unfreeze_function = Conv_oracle.unfreeze;
-      init_function = Conv_oracle.init }
+let _ = Summary.declare_summary "Transparent constants and variables"
+  { Summary.freeze_function = Conv_oracle.freeze;
+    Summary.unfreeze_function = Conv_oracle.unfreeze;
+    Summary.init_function = Summary.nop }
 
 
 (* Generic reduction: reduction functions used in reduction tactics *)
@@ -148,7 +147,7 @@ let reduction_tab = ref String.Map.empty
 
 (* table of custom reduction expressions, synchronized,
    filled by command Declare Reduction *)
-let red_expr_tab = ref String.Map.empty
+let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction"
 
 let declare_reduction s f =
   if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
@@ -253,8 +252,3 @@ let inReduction : bool * string * red_expr -> obj =
 
 let declare_red_expr locality s expr =
     Lib.add_anonymous_leaf (inReduction (locality,s,expr))
-
-let _ = declare_summary "Declare Reduction"
-  { freeze_function = (fun () -> !red_expr_tab);
-    unfreeze_function = ((:=) red_expr_tab);
-    init_function = (fun () -> red_expr_tab := String.Map.empty) }
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 38a616dde..39e0c653c 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -58,16 +58,7 @@ module HintDN = Term_dnet.Make(HintIdent)(HintOpt)
 
 (* Summary and Object declaration *)
 let rewtab =
-  ref (String.Map.empty : HintDN.t String.Map.t)
-
-let _ =
-  let init () = rewtab := String.Map.empty in
-  let freeze () = !rewtab in
-  let unfreeze fs = rewtab := fs in
-  Summary.declare_summary "autorewrite"
-    { Summary.freeze_function   = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function     = init }
+  Summary.ref (String.Map.empty : HintDN.t String.Map.t) ~name:"autorewrite"
 
 let raw_find_base bas = String.Map.find bas !rewtab
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 45a705f35..8da15e8da 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -276,20 +276,13 @@ let make_hints g st only_classes sign =
     (PathEmpty, []) sign
   in Hint_db.add_list hintlist (Hint_db.empty st true)
 
-let autogoal_hints_cache : (bool * Environ.named_context_val * hint_db) option ref = ref None
+let autogoal_hints_cache
+    : (bool * Environ.named_context_val * hint_db) option ref
+    = Summary.ref None ~name:"autogoal-hints-cache"
 let freeze () = !autogoal_hints_cache
 let unfreeze v = autogoal_hints_cache := v
-let init () = autogoal_hints_cache := None
 
-let _ = init ()
-
-let _ =
-  Summary.declare_summary "autogoal-hints-cache"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
-    
-let make_autogoal_hints = 
+let make_autogoal_hints =
   fun only_classes ?(st=full_transparent_state) g ->
     let sign = pf_filtered_hyps g in
       match freeze () with
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a8188d582..0ec167873 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -406,7 +406,6 @@ END
 
 open Tactics
 open Glob_term
-open Summary
 open Libobject
 open Lib
 
@@ -415,8 +414,8 @@ open Lib
      x R y -> x == z -> z R y    (in the left table)
 *)
 
-let transitivity_right_table = ref []
-let transitivity_left_table = ref []
+let transitivity_right_table = Summary.ref [] ~name:"transitivity-steps-r"
+let transitivity_left_table = Summary.ref [] ~name:"transitivity-steps-l"
 
 (* [step] tries to apply a rewriting lemma; then apply [tac] intended to
    complete to proof of the last hypothesis (assumed to state an equality) *)
@@ -448,24 +447,6 @@ let inTransitivity : bool * constr -> obj =
     subst_function = subst_transitivity_lemma;
     classify_function = (fun o -> Substitute o) }
 
-(* Synchronisation with reset *)
-
-let freeze () = !transitivity_left_table, !transitivity_right_table
-
-let unfreeze (l,r) =
-  transitivity_left_table := l;
-  transitivity_right_table := r
-
-let init () =
-  transitivity_left_table := [];
-  transitivity_right_table := []
-
-let _ =
-  declare_summary "transitivity-steps"
-    { freeze_function = freeze;
-      unfreeze_function = unfreeze;
-      init_function = init }
-
 (* Main entry points *)
 
 let add_transitivity_lemma left lem =
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index db2c19f00..d1abdd0af 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -155,17 +155,12 @@ let lookup_tactic s =
 
 (* Summary and Object declaration *)
 
-let mactab = ref (Gmap.empty : (ltac_constant,glob_tactic_expr) Gmap.t)
+let mactab =
+  Summary.ref (Gmap.empty : (ltac_constant,glob_tactic_expr) Gmap.t)
+    ~name:"tactic-definition"
 
 let lookup_ltacref r = Gmap.find r !mactab
 
-let _ =
-  Summary.declare_summary "tactic-definition"
-    { Summary.freeze_function   = (fun () -> !mactab);
-      Summary.unfreeze_function = (fun fs -> mactab := fs);
-      Summary.init_function     = (fun () -> mactab := Gmap.empty); }
-
-
 
 (* We have identifier <| global_reference <| constr *)
 
diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml
index 561485833..7a13890b5 100644
--- a/tactics/tactic_option.ml
+++ b/tactics/tactic_option.ml
@@ -10,12 +10,17 @@ open Libobject
 open Pp
 
 let declare_tactic_option ?(default=Tacexpr.TacId []) name =
-  let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref default in
-  let default_tactic : Proof_type.tactic ref = ref (Tacinterp.eval_tactic !default_tactic_expr) in
-  let locality = ref false in
-  let set_default_tactic local t = 
+  let locality = Summary.ref false ~name:(name^"-locality") in
+  let default_tactic_expr : Tacexpr.glob_tactic_expr ref =
+    Summary.ref default ~name:(name^"-default-tacexpr")
+  in
+  let default_tactic : Proof_type.tactic ref =
+    ref (Tacinterp.eval_tactic !default_tactic_expr)
+  in
+  let set_default_tactic local t =
     locality := local;
-    default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t 
+    default_tactic_expr := t;
+    default_tactic := Tacinterp.eval_tactic t
   in
   let cache (_, (local, tac)) = set_default_tactic local tac in
   let load (_, (local, tac)) =
@@ -43,12 +48,4 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
     Pptactic.pr_glob_tactic (Global.env ()) !default_tactic_expr ++
       (if !locality then str" (locally defined)" else str" (globally defined)")
   in
-  let freeze () = !locality, !default_tactic_expr in
-  let unfreeze (local, t) = set_default_tactic local t in
-  let init () = () in
-    Summary.declare_summary name
-      { Summary.freeze_function = freeze;
-        Summary.unfreeze_function = unfreeze;
-        Summary.init_function = init };
-    put, get, print
-      
+  put, get, print
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 5acbb78b7..5413e69a0 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -32,7 +32,7 @@ type individual_scheme_object_function = inductive -> constr
 
 type 'a scheme_kind = string
 
-let scheme_map = ref Indmap.empty
+let scheme_map = Summary.ref Indmap.empty ~name:"Schemes"
 
 let cache_one_scheme kind (ind,const) =
   let map = try Indmap.find ind !scheme_map with Not_found -> String.Map.empty in
@@ -61,19 +61,6 @@ let inScheme : string * (inductive * constant) array -> obj =
 		    discharge_function = discharge_scheme}
 
 (**********************************************************************)
-(* Saving/restoring the table of scheme *)
-
-let freeze_schemes () = !scheme_map
-let unfreeze_schemes sch = scheme_map := sch
-let init_schemes () = scheme_map := Indmap.empty
-
-let _ =
-  Summary.declare_summary "Schemes"
-    { Summary.freeze_function = freeze_schemes;
-      Summary.unfreeze_function = unfreeze_schemes;
-      Summary.init_function = init_schemes }
-
-(**********************************************************************)
 (* The table of scheme building functions *)
 
 type individual
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 7a0c498b2..8c7c377bf 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -446,23 +446,8 @@ let map_first m =
     assert(false)
   with Found x -> x
 
-let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
-
-let freeze () = !from_prg
-let unfreeze v = from_prg := v
-let init () = from_prg := ProgMap.empty
-
-(** Beware: if this code is dynamically loaded via dynlink after the start
-    of Coq, then this [init] function will not be run by [Lib.init ()].
-    Luckily, here we can launch [init] at load-time. *)
-
-let _ = init ()
-
-let _ =
-  Summary.declare_summary "program-tcc-table"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+let from_prg : program_info ProgMap.t ref =
+  Summary.ref ProgMap.empty ~name:"program-tcc-table"
 
 let close sec =
   if not (ProgMap.is_empty !from_prg) then