diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp index 6e2713b09b..5d5aab6d7a 100644 --- a/src/library/compiler/compiler.cpp +++ b/src/library/compiler/compiler.cpp @@ -273,6 +273,7 @@ void initialize_compiler() { register_trace_class({"compiler", "cce"}); register_trace_class({"compiler", "simp"}); register_trace_class({"compiler", "simp_detail"}); + register_trace_class({"compiler", "simp_float_cases"}); register_trace_class({"compiler", "elim_dead_let"}); register_trace_class({"compiler", "cse"}); register_trace_class({"compiler", "specialize"}); diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp index 8bbc34ec48..b5312ea42d 100644 --- a/src/library/compiler/csimp.cpp +++ b/src/library/compiler/csimp.cpp @@ -456,7 +456,7 @@ class csimp_fn { } } } - lean_trace(name({"compiler", "simp"}), + lean_trace(name({"compiler", "simp_float_cases"}), tout() << "mk_join " << fvar << "\n" << c << "\n---\n" << e << "\n======>\n" << mk_app(fn, args) << "\n";); return mk_app(fn, args); @@ -653,7 +653,7 @@ class csimp_fn { new_minor = mk_minor_lambda(zs, new_minor); c_args[minor_idx] = new_minor; } - lean_trace(name({"compiler", "simp"}), + lean_trace(name({"compiler", "simp_float_cases"}), tout() << "float_cases_on [" << get_lcnf_size(env(), e) << "]\n" << c << "\n----\n" << e << "\n=====>\n" << mk_app(c_fn, c_args) << "\n";); return mk_app(c_fn, c_args);