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

4 files changed, 10 insertions, 32 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