diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8efe3614e..fc0e5beaa 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1347,19 +1347,10 @@ let _ = optwrite = Flags.make_universe_polymorphism } let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "use of virtual machine inside the kernel"; - optkey = ["Virtual";"Machine"]; - optread = (fun () -> Vconv.use_vm ()); - optwrite = (fun b -> Vconv.set_use_vm b) } - -let _ = declare_int_option { optsync = true; optdepr = false; - optname = "the level of inling duging functor application"; + optname = "the level of inlining during functor application"; optkey = ["Inline";"Level"]; optread = (fun () -> Some (Flags.get_inline_level ())); optwrite = (fun o -> |