michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): make sure the proof state bit "report errors" is

Browse source 
set in the beginning of each begin-end element

see discussion at #583
This commit is contained in:
Leonardo de Moura 2015-05-07 09:43:03 -07:00
parent 5798ac43de
commit e0b7017435
2 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/frontends/lean/elaborator.cpp
View file

@ -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) {

1
src/library/tactic/rewrite_tactic.cpp
View file

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