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

chore(library/tactic/simplify): remove dead option

Browse source
This commit is contained in:
Leonardo de Moura 2017-06-21 15:32:08 -07:00
parent 629d5ebbe8
commit fd17a19a23
2 changed files with 0 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/inductive_compiler/nested.cpp
View file

@ -1554,7 +1554,6 @@ class add_nested_inductive_decl_fn {
cfg.m_canonize_proofs = false;
cfg.m_use_axioms = false;
cfg.m_zeta = false;
cfg.m_use_matcher = false;
return cfg;
}

3
src/library/tactic/simplify.h
View file

@ -37,9 +37,6 @@ struct simp_config {
bool m_beta;
bool m_eta;
bool m_proj;
/* The following option should be removed as soon as we
refactor the inductive compiler. */
bool m_use_matcher{true};
simp_config();
simp_config(vm_obj const & o);
};