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

chore(library/equations_compiler/elim_match): add cases/induction tactic error message to trace

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-04 17:33:26 -07:00
parent 6c80f7b75c
commit 120bffce25
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/equations_compiler/elim_match.cpp
View file

@ -620,8 +620,8 @@ struct elim_match_fn {
lean_assert(length(new_goals) == length(new_goal_cnames));
lean_assert(length(new_goals) == length(ilist));
lean_assert(length(new_goals) == length(slist));
} catch (exception &) {
trace_match(tout() << "dependent pattern matching step failed\n";);
} catch (exception & ex) {
trace_match(tout() << "dependent pattern matching step failed\n" << ex.what() << "\n";);
throw_error("equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' "
"for additional details)");
}