selective join/export of the safe_environment

This generalizes the BuildVi flag and lets one choose which
opaque proofs are done and which not.

4 files changed, 11 insertions, 11 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index bf6fe9f0d..30cac7771 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -873,9 +873,9 @@ let start_library dir =
   Lib.start_compilation dir mp;
   Lib.add_frozen_state ()
 
-let end_library dir =
+let end_library ?except dir =
   let oname = Lib.end_compilation_checks dir in
-  let mp,cenv,ast = Global.export dir in
+  let mp,cenv,ast = Global.export ?except dir in
   let prefix, lib_stack = Lib.end_compilation oname in
   assert (ModPath.equal mp (MPfile dir));
   let substitute, keep, _ = Lib.classify_segment lib_stack in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index c5dc5a7f5..34d79087d 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -80,7 +80,7 @@ val get_library_symbols_tbl : library_name -> Nativecode.symbol array
 val start_library : library_name -> unit
 
 val end_library :
-  library_name ->
+  ?except:Future.UUIDSet.t -> library_name ->
     Safe_typing.compiled_library * library_objects * Safe_typing.native_library
 
 (** [really_import_module mp] opens the module [mp] (in a Caml sense).
diff --git a/library/global.ml b/library/global.ml
index 49f78e495..68fb1c46f 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -16,15 +16,14 @@ module GlobalSafeEnv : sig
 
   val safe_env : unit -> Safe_typing.safe_environment
   val set_safe_env : Safe_typing.safe_environment -> unit
-  val join_safe_environment : unit -> unit
+  val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
 
 end = struct
 
 let global_env = ref Safe_typing.empty_environment
 
-let join_safe_environment () =
-  if !Flags.compilation_mode <> Flags.BuildVi then
-    global_env := Safe_typing.join_safe_environment !global_env
+let join_safe_environment ?except () =
+  global_env := Safe_typing.join_safe_environment ?except !global_env
 
 let () =
   Summary.declare_summary "Global environment"
@@ -47,7 +46,8 @@ let set_safe_env e = global_env := e
 end
 
 let safe_env = GlobalSafeEnv.safe_env
-let join_safe_environment = GlobalSafeEnv.join_safe_environment
+let join_safe_environment ?except () =
+  GlobalSafeEnv.join_safe_environment ?except ()
 
 let env () = Safe_typing.env_of_safe_env (safe_env ())
 
@@ -140,7 +140,7 @@ let mind_of_delta_kn kn =
 (** Operations on libraries *)
 
 let start_library dir = globalize (Safe_typing.start_library dir)
-let export s = Safe_typing.export !Flags.compilation_mode (safe_env ()) s
+let export ?except s = Safe_typing.export ?except (safe_env ()) s
 let import c u d = globalize (Safe_typing.import c u d)
 
 
diff --git a/library/global.mli b/library/global.mli
index 8ae77a9e4..348f0be99 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -98,7 +98,7 @@ val universes_of_constant_body :
 (** {6 Compiled libraries } *)
 
 val start_library : DirPath.t -> module_path
-val export : DirPath.t ->
+val export : ?except:Future.UUIDSet.t -> DirPath.t ->
   module_path * Safe_typing.compiled_library * Safe_typing.native_library
 val import :
   Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest ->
@@ -111,7 +111,7 @@ val import :
 
 val env_of_context : Environ.named_context_val -> Environ.env
 
-val join_safe_environment : unit -> unit
+val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
 
 val is_polymorphic : Globnames.global_reference -> bool
 val is_template_polymorphic : Globnames.global_reference -> bool