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

1 files changed, 3 insertions, 12 deletions

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