diff options
| -rw-r--r-- | toplevel/vernacentries.ml | 9 |
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 ())); |