Adding a toplevel option allowing to deactivate the term sharing in kernel

reduction.

1 files changed, 9 insertions, 0 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8e424a96ff..65326774f9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1245,6 +1245,15 @@ let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
+      optname  = "kernel term sharing";
+      optkey   = ["Kernel"; "Term"; "Sharing"];
+      optread  = (fun () -> !Closure.share);
+      optwrite = (fun b -> Closure.share := b) }
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
       optname  = "use of boxed values";
       optkey   = ["Boxed";"Values"];
       optread  = (fun _ -> not (Vm.transp_values ()));