From e0b7017435e5c34ecc3a5b756f468a4bb3a97e07 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 7 May 2015 09:43:03 -0700
Subject: [PATCH] feat(frontends/lean): make sure the proof state bit "report
 errors" is set in the beginning of each begin-end element

see discussion at #583
---
 src/frontends/lean/elaborator.cpp     | 1 +
 src/library/tactic/rewrite_tactic.cpp | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 3c829ad00..d05f30b35 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1764,6 +1764,7 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr
             expr new_ptac = subst.instantiate_all(ptac);
             if (auto tac = pre_tactic_to_tactic(new_ptac)) {
                 try {
+                    ps = ps.update_report_failure(true);
                     proof_state_seq seq = (*tac)(env(), ios(), ps);
                     auto r = seq.pull();
                     if (!r) {
diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 21d4780a0..e736dfefa 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -1422,6 +1422,7 @@ class rewrite_fn {
                                                r = format("invalid 'rewrite' tactic, "
                                                              "rewrite step produced type incorrect term");
                                                if (saved_ex) {
+                                                   r += line();
                                                    r += saved_ex->pp(fmt);
                                                    r += line();
                                                }