diff options
| author | coqbot-app[bot] | 2021-02-25 16:46:41 +0000 |
|---|---|---|
| committer | GitHub | 2021-02-25 16:46:41 +0000 |
| commit | 24e94b3dac66510e6d57b9f55f9a4e3e84fd6e54 (patch) | |
| tree | 5befd0a43d5973f3c0707c65a90265121db8047c /kernel/nativeconv.ml | |
| parent | 6ef58b0e9348d49ccf456d9fd475368c3dc1aafa (diff) | |
| parent | 0772562f1ef66ee69677456963187d6ff736b0bf (diff) | |
Merge PR #13202: Infrastructure for fine-grained debug flags
Reviewed-by: gares
Ack-by: herbelin
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
Ack-by: ejgallego
Diffstat (limited to 'kernel/nativeconv.ml')
| -rw-r--r-- | kernel/nativeconv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index d77ee759c6..7e73725c6c 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -159,12 +159,12 @@ let native_conv_gen pb sigma env univs t1 t2 = let ml_filename, prefix = get_ml_filename () in let code, upds = mk_conv_code env sigma prefix t1 t2 in let fn = compile ml_filename code ~profile:false in - if !Flags.debug then Feedback.msg_debug (Pp.str "Running test..."); + debug_native_compiler (fun () -> Pp.str "Running test..."); let t0 = Sys.time () in call_linker ~fatal:true ~prefix fn (Some upds); let t1 = Sys.time () in let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in - if !Flags.debug then Feedback.msg_debug (Pp.str time_info); + debug_native_compiler (fun () -> Pp.str time_info); (* TODO change 0 when we can have de Bruijn *) fst (conv_val env pb 0 !rt1 !rt2 univs) |