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.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'library/global.mli') 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 -- cgit v1.2.3