diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-09 23:58:56 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-02 06:57:55 +0200 |
| commit | ce9b17821a3be3dee7fa7e49c35edaefc658b965 (patch) | |
| tree | 9466d4125f446a1483af29201026ca9734522014 /kernel/cbytegen.ml | |
| parent | f29f8f80c8ad94576c7a36f3f638866c208338a0 (diff) | |
[lib] Move global options to their proper place.
Recent commits introduced global flags, but these should be
module-specific so relocating.
Global flags are deprecated, and for 8.9 `Lib.Flags` will be reduced
to the truly global stuff.
Diffstat (limited to 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 0766f49b3..dfc6ff23f 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -832,6 +832,8 @@ let is_univ_copy max u = else false +let dump_bytecode = ref false + let dump_bytecodes init code fvs = let open Pp in (str "code =" ++ fnl () ++ @@ -875,7 +877,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c = reloc, init_code in let fv = List.rev (!(reloc.in_env).fv_rev) in - (if !Flags.dump_bytecode then + (if !dump_bytecode then Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) with TooLargeInductive msg -> |