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

feat(frontends/lean/tactic_evaluator): better error message

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-05 13:32:59 -08:00
parent f008e623e9
commit b0de6723ec
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/tactic_evaluator.cpp
View file

@ -189,7 +189,10 @@ pair<vm_obj, tactic_state> tactic_evaluator::mk_smt_state(tactic_state const & s
if (is_tactic_result_success(r)) {
return mk_pair(get_tactic_result_value(r), to_tactic_state(get_tactic_result_state(r)));
}
throw elaborator_exception(ref, "failed to execute smt_tactic, initial smt_state could not be constructed");
tactic_exception_info info = *is_tactic_exception(S, r);
throw elaborator_exception(ref,
format("failed to execute smt_tactic, initial smt_state could not be constructed, nested error:") +
line() + std::get<0>(info));
}
pair<vm_obj, tactic_state> tactic_evaluator::execute_smt_begin_end_core(vm_obj const & ss, tactic_state const & ts, buffer<expr> const & tactics, expr const & ref) {