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

fix(library/tactic/tactic_state): VM closure arguments should be in reverse order

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-13 13:23:46 -07:00
parent 290a925c5f
commit 3962d9b021
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -180,7 +180,7 @@ vm_obj mk_tactic_exception(throwable const & ex) {
vm_obj mk_tactic_exception(format const & fmt) {
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(), mk_vm_unit(), mk_vm_unit(), to_obj(fmt)));
return mk_tactic_exception(mk_vm_closure(K.get_idx(), to_obj(fmt), mk_vm_unit(), mk_vm_unit()));
}
vm_obj mk_tactic_exception(char const * msg) {