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

fix(library/tactic/tactic_state): do not assume combinator.K is in the environment

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-28 16:48:53 +01:00
parent 9d7a75d0e2
commit 1c2804256e
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/tactic/tactic_state.cpp
View file

@ -209,8 +209,12 @@ vm_obj mk_tactic_exception(throwable const & ex, tactic_state const & s) {
vm_obj mk_tactic_exception(format const & fmt, tactic_state const & s) {
vm_state const & S = get_vm_state();
vm_decl K = *S.get_decl(get_combinator_K_name());
return mk_tactic_exception(mk_vm_closure(K.get_idx(), to_obj(fmt), mk_vm_unit(), mk_vm_unit()), s);
if (optional<vm_decl> K = S.get_decl(get_combinator_K_name())) {
return mk_tactic_exception(mk_vm_closure(K->get_idx(), to_obj(fmt), mk_vm_unit(), mk_vm_unit()), s);
} else {
throw exception("failed to create tactic exceptional result, combinator.K is not in the environment, "
"this can happen when users are hacking the init folder");
}
}
vm_obj mk_tactic_exception(char const * msg, tactic_state const & s) {