From 05add2ea02a96cf34e626ddf341cdebcb839adfb Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Tue, 1 Nov 2016 17:26:48 -0700 Subject: [PATCH] fix(library/tactic/simplify.cpp): fix debug tracing names --- src/library/tactic/simplify.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index cee384705a..4d9c40c62c 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -495,12 +495,12 @@ simp_result simplify_core_fn::rewrite(expr const & e) { simp_result simplify_core_fn::rewrite(expr const & e, simp_lemma const & sl) { tmp_type_context tmp_ctx(m_ctx, sl.get_num_umeta(), sl.get_num_emeta()); if (!tmp_ctx.is_def_eq(e, sl.get_lhs())) { - lean_trace_d(name({"debug", "simplify", "rewrite"}), tout() << "fail to unify: " << sl.get_id() << "\n";); + lean_trace_d(name({"debug", "simplify", "try_rewrite"}), tout() << "fail to unify: " << sl.get_id() << "\n";); return simp_result(e); } if (!instantiate_emetas(tmp_ctx, sl.get_num_emeta(), sl.get_emetas(), sl.get_instances())) { - lean_trace_d(name({"debug", "simplify", "rewrite"}), tout() << "fail to instantiate emetas: " << + lean_trace_d(name({"debug", "simplify", "try_rewrite"}), tout() << "fail to instantiate emetas: " << sl.get_id() << "\n";); return simp_result(e); }