max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/tactic/simplify.cpp): fix debug tracing names

Browse source
This commit is contained in:
Daniel Selsam 2016-11-01 17:26:48 -07:00 • committed by Leonardo de Moura
parent b22192eee1
commit 05add2ea02
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/tactic/simplify.cpp
View file

@ -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);
}