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

fix(library/tactic/congruence/congruence_tactics): stupid mistake

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-22 20:54:20 -08:00
parent 6329afc121
commit 104ee1b120
3 changed files with 6 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/tactic/congruence/congruence_tactics.cpp
View file

@ -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);
}

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

@ -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);

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

@ -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); \