diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-12 16:39:32 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-17 15:05:04 +0100 |
| commit | 5f2f22e7ff5d53e3258affa0e0e41666d5e0691d (patch) | |
| tree | a8a52df78e46d9b663f5583f36aa1afe401fdd05 | |
| parent | eb1eddf24932232890e32acf0fc4ff418ad0c281 (diff) | |
Global: export the name of the summary entry
In this way one can make surgery on the system states, like
checking if two frozen states have the same environment (i.e.
no running "abstract" in between)
| -rw-r--r-- | library/global.ml | 4 | ||||
| -rw-r--r-- | library/global.mli | 2 |
2 files changed, 5 insertions, 1 deletions
diff --git a/library/global.ml b/library/global.ml index 68fb1c46f..9aaeffd71 100644 --- a/library/global.ml +++ b/library/global.ml @@ -12,6 +12,8 @@ open Environ (** We introduce here the global environment of the system, and we declare it as a synchronized table. *) +let global_env_summary_name = "Global environment" + module GlobalSafeEnv : sig val safe_env : unit -> Safe_typing.safe_environment @@ -26,7 +28,7 @@ let join_safe_environment ?except () = global_env := Safe_typing.join_safe_environment ?except !global_env let () = - Summary.declare_summary "Global environment" + Summary.declare_summary global_env_summary_name { Summary.freeze_function = (function | `Yes -> join_safe_environment (); !global_env | `No -> !global_env diff --git a/library/global.mli b/library/global.mli index 348f0be99..444ea9f7f 100644 --- a/library/global.mli +++ b/library/global.mli @@ -139,3 +139,5 @@ val set_strategy : Names.constant Names.tableKey -> Conv_oracle.level -> unit val current_dirpath : unit -> Names.dir_path val with_global : (Environ.env -> Names.dir_path -> 'a Univ.in_universe_context_set) -> 'a + +val global_env_summary_name : string |