From 1c70514231ebc51836bc4e558869ebed57559e8e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 21 Jun 2015 16:50:45 -0700 Subject: [PATCH] feat(frontends/lean/structure_cmd): disable conversion optimization for automatically generated coercions --- src/frontends/lean/structure_cmd.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 92f73ecd3f..f18152a178 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -815,7 +815,8 @@ struct structure_cmd_fn { } coercion_value = Fun(m_params, Fun(st, coercion_value)); 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 = set_reducible(m_env, coercion_name, reducible_status::Reducible); save_def_info(coercion_name);