diff options
| author | Gaëtan Gilbert | 2020-08-18 13:07:54 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-18 13:07:54 +0200 |
| commit | 4ee0cedff7726a56ebd53125995a7ae131660b4a (patch) | |
| tree | f5049f849a27b518f5c27298058df620a0ca38b3 /vernac/vernacentries.ml | |
| parent | aa926429727f1f6b5ef07c8912f2618d53f6d155 (diff) | |
Rename VM-related kernel/cfoo files to kernel/vmfoo
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 d540e7f93d..4262563686 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1511,15 +1511,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 |
