diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp index 787f04bb9..0430d8209 100644 --- a/src/frontends/lean/frontend_elaborator.cpp +++ b/src/frontends/lean/frontend_elaborator.cpp @@ -507,7 +507,7 @@ public: } }; -frontend_elaborator::frontend_elaborator(environment const & env):m_ptr(new imp(env)) {} +frontend_elaborator::frontend_elaborator(environment const & env):m_ptr(std::make_shared(env)) {} frontend_elaborator::~frontend_elaborator() {} std::pair frontend_elaborator::operator()(expr const & e) { return m_ptr->elaborate(e); } std::tuple frontend_elaborator::operator()(name const & n, expr const & t, expr const & e) { diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index c979ee4cd..97eb697b2 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -461,14 +461,14 @@ environment_cell::~environment_cell() { } environment::environment(): - m_ptr(new environment_cell()) { + m_ptr(std::make_shared()) { m_ptr->m_this = m_ptr; m_ptr->m_type_checker.reset(new type_checker(*this)); } // used when creating a new child environment environment::environment(std::shared_ptr const & parent, bool): - m_ptr(new environment_cell(parent)) { + m_ptr(std::make_shared(parent)) { m_ptr->m_this = m_ptr; m_ptr->m_type_checker.reset(new type_checker(*this)); } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 806594855..dd30e6429 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -78,10 +78,10 @@ class environment_cell { bool already_imported(name const & n) const; bool mark_imported_core(name n); - environment_cell(std::shared_ptr const & parent); public: environment_cell(); + environment_cell(std::shared_ptr const & parent); ~environment_cell(); /** \brief Return true iff this environment has children environments. */ diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp index 7fbe2d58b..989b78284 100644 --- a/src/library/io_state.cpp +++ b/src/library/io_state.cpp @@ -11,15 +11,15 @@ Author: Leonardo de Moura namespace lean { io_state::io_state(): m_formatter(mk_simple_formatter()), - m_regular_channel(new stdout_channel()), - m_diagnostic_channel(new stderr_channel()) { + m_regular_channel(std::make_shared()), + m_diagnostic_channel(std::make_shared()) { } io_state::io_state(options const & opts, formatter const & fmt): m_options(opts), m_formatter(fmt), - m_regular_channel(new stdout_channel()), - m_diagnostic_channel(new stderr_channel()) { + m_regular_channel(std::make_shared()), + m_diagnostic_channel(std::make_shared()) { } io_state::~io_state() {} diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 60382a0ba..211a0851c 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -176,7 +176,7 @@ tactic trace_state_tactic() { tactic suppress_trace(tactic const & t) { return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { io_state new_io(io); - std::shared_ptr out(new string_output_channel()); + std::shared_ptr out(std::make_shared()); new_io.set_diagnostic_channel(out); return t(env, new_io, s); }); diff --git a/src/tests/frontends/lean/pp.cpp b/src/tests/frontends/lean/pp.cpp index 711abbb83..5f6cda659 100644 --- a/src/tests/frontends/lean/pp.cpp +++ b/src/tests/frontends/lean/pp.cpp @@ -72,7 +72,7 @@ static void tst4() { static void tst5() { environment env; io_state ios; init_frontend(env, ios); - std::shared_ptr out(new string_output_channel()); + std::shared_ptr out(std::make_shared()); ios.set_regular_channel(out); ios.set_option(name{"pp", "unicode"}, true); ios.set_option(name{"lean", "pp", "notation"}, true); @@ -92,7 +92,7 @@ static expr mk_deep(unsigned depth) { static void tst6() { environment env; io_state ios; init_frontend(env, ios); - std::shared_ptr out(new string_output_channel()); + std::shared_ptr out(std::make_shared()); ios.set_regular_channel(out); expr t = mk_deep(10); ios.set_option(name{"lean", "pp", "max_depth"}, 5); diff --git a/src/util/script_state.cpp b/src/util/script_state.cpp index 9241f65d3..56b9e5db6 100644 --- a/src/util/script_state.cpp +++ b/src/util/script_state.cpp @@ -133,7 +133,7 @@ script_state to_script_state(lua_State * L) { } script_state::script_state(): - m_ptr(new imp()) { + m_ptr(std::make_shared()) { m_ptr->save_weak_ptr(m_ptr); }