diff options
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4e08a40d6b..540e85621a 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1516,15 +1516,15 @@ let () = declare_bool_option { optdepr = false; optkey = ["Dump";"Bytecode"]; - optread = (fun () -> !Cbytegen.dump_bytecode); - optwrite = (:=) Cbytegen.dump_bytecode } + optread = (fun () -> !Vmbytegen.dump_bytecode); + optwrite = (:=) Vmbytegen.dump_bytecode } let () = declare_bool_option { optdepr = false; optkey = ["Dump";"Lambda"]; - optread = (fun () -> !Clambda.dump_lambda); - optwrite = (:=) Clambda.dump_lambda } + optread = (fun () -> !Vmlambda.dump_lambda); + optwrite = (:=) Vmlambda.dump_lambda } let () = declare_bool_option |