From 52e4f029c43320bee5e1e14a83ef6b1e3a51ae43 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 29 Jul 2019 14:03:52 +0200
Subject: [PATCH] [rmtmps] avoid useless computation when not debugging
---
src/kernel_internals/typing/rmtmps.ml | 15 +++++++++------
1 file changed, 9 insertions(+), 6 deletions(-)
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 8143accc84b..64ada096ee7 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -903,12 +903,15 @@ let removeUnusedTemps ?(isRoot : rootsFilter = isExportedRoot) ast =
(* mark everything reachable from the global roots *)
markReachable isRoot ast reachable_tbl;
- let elements =
- InfoHashtbl.fold (fun k v acc -> Format.asprintf "%a:%B" pp_info k v :: acc)
- reachable_tbl []
- in
- Kernel.debug ~dkey "reachable_tbl: %a"
- (Pretty_utils.pp_list ~sep:"@\n" Format.pp_print_string) elements;
+ Kernel.debug ~dkey "reachable_tbl: %t"
+ (fun fmt ->
+ let elements =
+ InfoHashtbl.fold (fun k v acc ->
+ Format.asprintf "%a:%B" pp_info k v :: acc)
+ reachable_tbl []
+ in
+ Format.fprintf fmt "%a"
+ (Pretty_utils.pp_list ~sep:"@\n" Format.pp_print_string) elements);
markReferenced ast;
--
GitLab