From c03250502376fc4e70e4bb64a6c414b8e8136351 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Aug 2016 13:45:04 -0700 Subject: [PATCH] chore(library/tactic/subst_tactic): missing '\n' in trace msg --- src/library/tactic/subst_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp index 5e8b38353b..213beaf929 100644 --- a/src/library/tactic/subst_tactic.cpp +++ b/src/library/tactic/subst_tactic.cpp @@ -33,7 +33,7 @@ bool check_hypothesis_in_context(metavar_context const & mctx, expr const & mvar expr subst(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx, expr const & mvar, expr const & H, bool symm, name_map * renames) { #define lean_subst_trace(CODE) lean_trace(name({"tactic", "subst"}), CODE) - #define lean_subst_trace_state(MVAR, MSG) lean_trace(name({"tactic", "subst"}), tactic_state S(env, opts, mctx, to_list(MVAR), MVAR); type_context TMP_CTX = mk_type_context_for(S, m); scope_trace_env _scope1(env, TMP_CTX); tout() << MSG << S.pp();) +#define lean_subst_trace_state(MVAR, MSG) lean_trace(name({"tactic", "subst"}), tactic_state S(env, opts, mctx, to_list(MVAR), MVAR); type_context TMP_CTX = mk_type_context_for(S, m); scope_trace_env _scope1(env, TMP_CTX); tout() << MSG << S.pp() << "\n";) lean_subst_trace_state(mvar, "initial:\n"); lean_assert(mctx.get_metavar_decl(mvar));