From 16251af41ad764f2437360bff09cd7ec9282a0c9 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 12 Nov 2024 14:10:37 +0100 Subject: [PATCH] restore printer --- src/lib/reasoners/matching.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml index 2ac57dc93..55e2bf782 100644 --- a/src/lib/reasoners/matching.ml +++ b/src/lib/reasoners/matching.ml @@ -157,9 +157,11 @@ module Make (X : Arg) : S with type theory = X.t = struct Ty.print_subst sty let match_class_of t cl = - Log.debug (fun k -> k "class of '%a' is:@ %a" - E.print t - Fmt.(box @@ braces @@ iter ~sep:comma E.Set.iter E.print) cl) + if Options.get_debug_matching() >= 3 then + Log.debug (fun k -> k "class of '%a' is:@ %a" + E.print t + Fmt.(box @@ braces + @@ iter ~sep:comma E.Set.iter E.print) cl) let candidate_substitutions pat_info res = let open Matching_types in