Introduce Safe_typing.set_share_reduction

5 files changed, 13 insertions, 1 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 12f9592ab7..90b89995ee 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -194,6 +194,10 @@ let set_engagement c senv =
 let set_typing_flags c senv =
   { senv with env = Environ.set_typing_flags c senv.env }
 
+let set_share_reduction b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with share_reduction = b } senv
+
 (** Check that the engagement [c] expected by a library matches
     the current (initial) one *)
 let check_engagement env expected_impredicative_set =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 26fa91adbd..ea288b771e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -137,6 +137,7 @@ val add_constraints :
 (** Setting the type theory flavor *)
 val set_engagement : Declarations.engagement -> safe_transformer0
 val set_typing_flags : Declarations.typing_flags -> safe_transformer0
+val set_share_reduction : bool -> safe_transformer0
 
 (** {6 Interactive module functions } *)
 
diff --git a/library/global.ml b/library/global.ml
index 009f498a9e..6461b4c37f 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -183,3 +183,6 @@ 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_share_reduction b =
+  globalize0 (Safe_typing.set_share_reduction b)
diff --git a/library/global.mli b/library/global.mli
index 5b0ff11b71..762a3f006d 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -150,6 +150,10 @@ val register_inline : Constant.t -> unit
 
 val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit
 
+(** {6 Conversion settings } *)
+
+val set_share_reduction : bool -> unit
+
 (* Modifies the global state, registering new universes *)
 
 val current_modpath : unit -> ModPath.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4df50a5e23..5eace14cbf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1536,7 +1536,7 @@ let _ =
       optname  = "kernel term sharing";
       optkey   = ["Kernel"; "Term"; "Sharing"];
       optread  = (fun () -> (Global.typing_flags ()).Declarations.share_reduction);
-      optwrite = (fun b -> Global.set_typing_flags { (Global.typing_flags ()) with Declarations.share_reduction = b }) }
+      optwrite = Global.set_share_reduction }
 
 let _ =
   declare_bool_option