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

feat(frontends/lean/structure_cmd): disable conversion optimization for automatically generated coercions

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-21 16:50:45 -07:00
parent aeea8f83c4
commit 1c70514231
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/structure_cmd.cpp
View file

@ -815,7 +815,8 @@ struct structure_cmd_fn {
} }
coercion_value = Fun(m_params, Fun(st, coercion_value)); coercion_value = Fun(m_params, Fun(st, coercion_value));
name coercion_name = coercion_names[i]; name coercion_name = coercion_names[i];
declaration coercion_decl = mk_definition(m_env, coercion_name, lnames, coercion_type, coercion_value); bool use_conv_opt = false;
declaration coercion_decl = mk_definition(m_env, coercion_name, lnames, coercion_type, coercion_value, use_conv_opt);
m_env = module::add(m_env, check(m_env, coercion_decl)); m_env = module::add(m_env, check(m_env, coercion_decl));
m_env = set_reducible(m_env, coercion_name, reducible_status::Reducible); m_env = set_reducible(m_env, coercion_name, reducible_status::Reducible);
save_def_info(coercion_name); save_def_info(coercion_name);