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, 1 insertions, 8 deletions

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