From 104ee1b1205c795d1ef4bf06c238aed4fb8a8b77 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Dec 2016 20:54:20 -0800 Subject: [PATCH] fix(library/tactic/congruence/congruence_tactics): stupid mistake --- src/library/tactic/congruence/congruence_tactics.cpp | 8 ++++++-- src/library/tactic/tactic_state.cpp | 6 ------ src/library/tactic/tactic_state.h | 2 -- 3 files changed, 6 insertions(+), 10 deletions(-) diff --git a/src/library/tactic/congruence/congruence_tactics.cpp b/src/library/tactic/congruence/congruence_tactics.cpp index a11a22ac40..af1ab5ad3a 100644 --- a/src/library/tactic/congruence/congruence_tactics.cpp +++ b/src/library/tactic/congruence/congruence_tactics.cpp @@ -62,14 +62,18 @@ vm_obj cc_state_mk_using_hs(vm_obj const & _s) { vm_obj cc_state_pp(vm_obj const & ccs, vm_obj const & _s) { tactic_state const & s = to_tactic_state(_s); - formatter fmt = mk_formatter_for(s); + type_context ctx = mk_type_context_for(s); + formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); + formatter fmt = fmtf(s.env(), s.get_options(), ctx); format r = to_cc_state(ccs).pp_eqcs(fmt); return mk_tactic_success(to_obj(r), s); } vm_obj cc_state_pp_eqc(vm_obj const & ccs, vm_obj const & e, vm_obj const & _s) { tactic_state const & s = to_tactic_state(_s); - formatter fmt = mk_formatter_for(s); + type_context ctx = mk_type_context_for(s); + formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); + formatter fmt = fmtf(s.env(), s.get_options(), ctx); format r = to_cc_state(ccs).pp_eqc(fmt, to_expr(e)); return mk_tactic_success(to_obj(r), s); } diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 3d0f194bb5..23ad9ea2c7 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -360,12 +360,6 @@ type_context mk_type_context_for(vm_obj const & s, vm_obj const & m) { return mk_type_context_for(to_tactic_state(s), to_transparency_mode(m)); } -formatter mk_formatter_for(tactic_state const & s) { - type_context ctx = mk_type_context_for(s); - formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); - return fmtf(s.env(), s.get_options(), ctx); -} - vm_obj tactic_infer_type(vm_obj const & e, vm_obj const & s0) { tactic_state const & s = to_tactic_state(s0); type_context ctx = mk_type_context_for(s); diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h index 4f4c1f0ddb..665d990d72 100644 --- a/src/library/tactic/tactic_state.h +++ b/src/library/tactic/tactic_state.h @@ -136,8 +136,6 @@ type_context mk_type_context_for(environment const & env, options const & o, type_context mk_type_context_for(vm_obj const & s); type_context mk_type_context_for(vm_obj const & s, vm_obj const & m); -formatter mk_formatter_for(tactic_state const & s); - #define lean_tactic_trace(N, S, Code) lean_trace(N, { \ type_context _ctx = mk_type_context_for(S); \ scope_trace_env _scope((S).env(), _ctx); \