From 5f2f22e7ff5d53e3258affa0e0e41666d5e0691d Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 12 Dec 2014 16:39:32 +0100
Subject: 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)
---
 library/global.ml  | 4 +++-
 library/global.mli | 2 ++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/library/global.ml b/library/global.ml
index 68fb1c46f7..9aaeffd71c 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 348f0be99f..444ea9f7f1 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
-- 
cgit v1.2.3