diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 882f21f7e..cc53c70d2 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -421,6 +421,9 @@ type_checker::type_checker(environment const & env, name_generator const & g, st m_memoize(memoize), m_params(nullptr) { } +type_checker::type_checker(environment const & env, name_generator const & g, bool memoize): + type_checker(env, g, mk_default_converter(env, optional(), memoize), memoize) {} + static name * g_tmp_prefix = nullptr; type_checker::type_checker(environment const & env): diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index c631cb7e4..2b1939c7f 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -119,8 +119,7 @@ public: memoize: if true, then inferred types are memoized/cached */ type_checker(environment const & env, name_generator const & g, std::unique_ptr && conv, bool memoize = true); - type_checker(environment const & env, name_generator const & g, bool memoize = true): - type_checker(env, g, mk_default_converter(env), memoize) {} + type_checker(environment const & env, name_generator const & g, bool memoize = true); type_checker(environment const & env); ~type_checker();