michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/unifier): remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-07 15:49:18 -07:00
parent 21ee0a5ff9
commit 88cd6e9a63
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/unifier.cpp
View file

@ -1313,8 +1313,6 @@ struct unifier_fn {
expr lhs_fn = get_app_rev_args(lhs, lhs_args); expr lhs_fn = get_app_rev_args(lhs, lhs_args);
expr rhs_fn = get_app_rev_args(rhs, rhs_args); expr rhs_fn = get_app_rev_args(rhs, rhs_args);
declaration d = *m_env.find(const_name(lhs_fn)); declaration d = *m_env.find(const_name(lhs_fn));
levels lhs_lvls = const_levels(lhs_fn);
levels rhs_lvls = const_levels(lhs_fn);
bool relax = relax_main_opaque(c); bool relax = relax_main_opaque(c);
expr lhs_fn_val = instantiate_value_univ_params(d, const_levels(lhs_fn)); expr lhs_fn_val = instantiate_value_univ_params(d, const_levels(lhs_fn));
expr rhs_fn_val = instantiate_value_univ_params(d, const_levels(rhs_fn)); expr rhs_fn_val = instantiate_value_univ_params(d, const_levels(rhs_fn));