From 2e66449feb40c1bc39459c6dfe417707dec2f4cd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Mar 2018 09:58:07 -0800 Subject: [PATCH] fix(library/tactic/tactic_state): build --- src/library/tactic/tactic_state.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index d134ba7452..e9984d9fb4 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -843,7 +843,7 @@ vm_obj io_run_tactic(vm_obj const &, vm_obj const & tac, vm_obj const &) { metavar_context(), local_context(), mk_true()); vm_obj r = invoke(tac, to_obj(s)); if (tactic::is_result_success(r)) { - return mk_io_result(tactic::get_result_value(r)); + return mk_io_result(tactic::get_success_value(r)); } else { return mk_io_failure("tactic failed"); // TODO(Leo): improve exception message }