diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 820903c41..35730eea0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1375,15 +1375,6 @@ let _ = 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 ())); - optwrite = (fun b -> Vm.set_transp_values (not b)) } - (* No more undo limit in the new proof engine. The command still exists for compatibility (e.g. with ProofGeneral) *) |