From 430dc21a288bc0ff8832dd0c6419a5ad2720f3dc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 21 Jun 2015 17:05:39 -0700 Subject: [PATCH] feat(library/composition_manager): disable conversion optimization for automatically generated compositions see issue #666 --- src/library/composition_manager.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/library/composition_manager.cpp b/src/library/composition_manager.cpp index ce6ed7d45..99a71a565 100644 --- a/src/library/composition_manager.cpp +++ b/src/library/composition_manager.cpp @@ -90,8 +90,9 @@ pair compose(environment const & env, type_checker & tc, name } ext.m_cache.insert(mk_pair(g, f), new_name); + bool use_conv_opt = false; environment new_env = module::add(env, check(env, mk_definition(env, new_name, f_decl.get_univ_params(), - new_type, new_val))); + new_type, new_val, use_conv_opt))); new_env = module::add(new_env, *g_key, [=](environment const &, serializer & s) { s << g << f << new_name; }); return mk_pair(update(new_env, ext), new_name); }