Turn the kernel reduction sharing flag into an argument passed in the cache.

We move the global declaration of that argument to the environment, and reuse
the Global module to handle this flag.

Note that the checker was not using this flag before this patch, and still
doesn't use it. This should probably be fixed in a later patch.

2 files changed, 10 insertions, 0 deletions

diff --git a/library/global.ml b/library/global.ml
index dcb20a280e..e833f71142 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -90,6 +90,7 @@ let push_context b c = globalize0 (Safe_typing.push_context b c)
 
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
 let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
+let typing_flags () = Environ.typing_flags (env ())
 let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
 let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
 let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
@@ -278,3 +279,9 @@ let register_inline c = globalize0 (Safe_typing.register_inline c)
 let set_strategy k l =
   GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l)
 
+let set_reduction_sharing b =
+  let env = safe_env () in
+  let flags = Environ.typing_flags (Safe_typing.env_of_safe_env env) in
+  let flags = { flags with Declarations.share_reduction = b } in
+  let env = Safe_typing.set_typing_flags flags env in
+  GlobalSafeEnv.set_safe_env env
diff --git a/library/global.mli b/library/global.mli
index b2a191ceeb..2819c187ed 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -30,6 +30,7 @@ val named_context : unit -> Constr.named_context
 (** Changing the (im)predicativity of the system *)
 val set_engagement : Declarations.engagement -> unit
 val set_typing_flags : Declarations.typing_flags -> unit
+val typing_flags : unit -> Declarations.typing_flags
 
 (** Variables, Local definitions, constants, inductive types *)
 
@@ -155,6 +156,8 @@ val register_inline : Constant.t -> unit
 
 val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit
 
+val set_reduction_sharing : bool -> unit
+
 (* Modifies the global state, registering new universes *)
 
 val current_modpath : unit -> ModPath.t