diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index abdf9dc79..3402f3b47 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -34,6 +34,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/class.h"
 #include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/info_manager.h"
+#include "frontends/lean/elaborator.h"
 
 #ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES
 #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true
@@ -121,6 +122,12 @@ public:
     expr operator()(expr const & e) { return apply(e); }
 };
 
+elaborator_env::elaborator_env(environment const & env, io_state const & ios, local_decls<level> const & lls,
+                               pos_info_provider const * pp, info_manager * info, bool check_unassigned):
+    m_env(env), m_ios(ios), m_lls(lls), m_pos_provider(pp), m_info_manager(info), m_check_unassigned(check_unassigned) {
+    m_use_local_instances = get_elaborator_local_instances(ios.get_options());
+}
+
 /** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */
 list<expr> get_local_instances(list<expr> const & ctx, name const & cls_name) {
     buffer<expr> buffer;
@@ -285,9 +292,7 @@ class elaborator {
     typedef name_map<expr> local_tactic_hints;
     typedef std::unique_ptr<type_checker> type_checker_ptr;
 
-    environment         m_env;
-    local_decls<level>  m_lls;
-    io_state            m_ios;
+    elaborator_env &    m_env;
     name_generator      m_ngen;
     type_checker_ptr    m_tc[2];
     mvar2meta           m_mvar2meta; // mapping from metavariable ?m to the (?m l_1 ... l_n) where [l_1 ... l_n] are the local constants
@@ -295,15 +300,11 @@ class elaborator {
     context             m_context; // current local context: a list of local constants
     context             m_full_context; // superset of m_context, it also contains non-contextual locals.
 
-    pos_info_provider * m_pos_provider; // optional expression position information used when reporting errors.
     constraint_vect     m_constraints; // constraints that must be solved for the elaborated term to be type correct.
     local_tactic_hints  m_local_tactic_hints; // mapping from metavariable name ?m to tactic expression that should be used to solve it.
                                               // this mapping is populated by the 'by tactic-expr' expression.
     name_set            m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned
-    bool                m_check_unassigned; // if true if display error messages if elaborated term still contains metavariables
-    bool                m_use_local_instances; // if true class-instance resolution will use the local context
     bool                m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent
-    info_manager *      m_info_manager;
     std::vector<type_info_data> m_pre_info_data;
 
     struct scope_ctx {
@@ -427,7 +428,7 @@ class elaborator {
         }
 
         optional<constraints> try_instance(name const & inst) {
-            auto decl   = m_elab.m_env.find(inst);
+            auto decl   = m_elab.env().find(inst);
             if (!decl)
                 return optional<constraints>();
             expr type   = decl->get_type();
@@ -487,7 +488,7 @@ class elaborator {
                 m_tactics          = tail(m_tactics);
                 proof_state ps(goals(goal(m_meta, m_meta_type)), substitution(), m_elab.m_ngen.mk_child());
                 try {
-                    m_tactic_result    = tac(m_elab.m_env, m_elab.m_ios, ps);
+                    m_tactic_result    = tac(m_elab.env(), m_elab.ios(), ps);
                     if (auto cs = get_next_tactic_result())
                         return cs;
                 } catch (exception &) {}
@@ -511,21 +512,24 @@ class elaborator {
     }
 
 public:
-    elaborator(environment const & env, local_decls<level> const & lls, list<expr> const & ctx, io_state const & ios, name_generator const & ngen,
-               pos_info_provider * pp, bool check_unassigned, info_manager * info):
-        m_env(env), m_lls(lls), m_ios(ios),
+    elaborator(elaborator_env & env, list<expr> const & ctx, name_generator const & ngen):
+        m_env(env),
         m_ngen(ngen),
         m_context(m_ngen, m_mvar2meta, ctx),
-        m_full_context(m_ngen, m_mvar2meta, ctx),
-        m_pos_provider(pp),
-        m_info_manager(info) {
+        m_full_context(m_ngen, m_mvar2meta, ctx) {
         m_relax_main_opaque = false;
-        m_tc[0] = mk_type_checker_with_hints(env, m_ngen.mk_child(), false);
-        m_tc[1] = mk_type_checker_with_hints(env, m_ngen.mk_child(), true);
-        m_check_unassigned = check_unassigned;
-        m_use_local_instances = get_elaborator_local_instances(ios.get_options());
+        m_tc[0] = mk_type_checker_with_hints(env.m_env, m_ngen.mk_child(), false);
+        m_tc[1] = mk_type_checker_with_hints(env.m_env, m_ngen.mk_child(), true);
     }
 
+    environment const & env() const { return m_env.m_env; }
+    io_state const & ios() const { return m_env.m_ios; }
+    local_decls<level> const & lls() const { return m_env.m_lls; }
+    bool use_local_instances() const { return m_env.m_use_local_instances; }
+    info_manager * infom() const { return m_env.m_info_manager; }
+    pos_info_provider const * pip() const { return m_env.m_pos_provider; }
+    bool check_unassigned() const { return m_env.m_check_unassigned; }
+
     expr mk_local(name const & n, expr const & t, binder_info const & bi) {
         return ::lean::mk_local(m_ngen.next(), n, t, bi);
     }
@@ -560,7 +564,7 @@ public:
     list<name> get_class_instances(expr const & type) {
         if (is_constant(get_app_fn(type))) {
             name const & c = const_name(get_app_fn(type));
-            return ::lean::get_class_instances(m_env, c);
+            return ::lean::get_class_instances(env(), c);
         } else {
             return list<name>();
         }
@@ -571,7 +575,7 @@ public:
         if (!is_constant(f))
             return false;
         name const & cls_name = const_name(f);
-        return ::lean::is_class(m_env, cls_name) || !empty(get_tactic_hints(m_env, cls_name));
+        return ::lean::is_class(env(), cls_name) || !empty(get_tactic_hints(env(), cls_name));
     }
 
     static expr instantiate_meta(expr const & meta, substitution & subst) {
@@ -585,11 +589,11 @@ public:
     /** \brief Return a 'failed to synthesize placholder' justification for the given
         metavariable application \c m of the form (?m l_1 ... l_k) */
     justification mk_failed_to_synthesize_jst(expr const & m) {
-        environment env = m_env;
+        environment _env = env();
         return mk_justification(m, [=](formatter const & fmt, substitution const & subst) {
                 substitution tmp(subst);
                 expr new_m    = instantiate_meta(m, tmp);
-                expr new_type = type_checker(env).infer(new_m);
+                expr new_type = type_checker(_env).infer(new_m);
                 proof_state ps(goals(goal(new_m, new_type)), substitution(), name_generator("dontcare"));
                 return format({format("failed to synthesize placeholder"), line(), ps.pp(fmt)});
             });
@@ -608,12 +612,12 @@ public:
             if (is_class(meta_type)) {
                 name const & cls_name = const_name(get_app_fn(meta_type));
                 list<expr> local_insts;
-                if (m_use_local_instances)
+                if (use_local_instances())
                     local_insts = get_local_instances(ctx, cls_name);
                 list<name>  insts = get_class_instances(meta_type);
                 list<tactic_hint_entry> tacs;
                 if (!s.is_assigned(mvar))
-                    tacs = get_tactic_hints(m_env, cls_name);
+                    tacs = get_tactic_hints(env(), cls_name);
                 if (empty(local_insts) && empty(insts) && empty(tacs))
                     return lazy_list<constraints>(); // nothing to be done
                 bool ignore_failure = false; // we are always strict with placeholders associated with classes
@@ -624,7 +628,7 @@ public:
                 // the an empty set of constraints.
                 return lazy_list<constraints>(constraints());
             } else {
-                list<tactic_hint_entry> tacs = get_tactic_hints(m_env);
+                list<tactic_hint_entry> tacs = get_tactic_hints(env());
                 bool ignore_failure = !is_strict;
                 return choose(std::make_shared<placeholder_elaborator>(*this, meta, meta_type, list<expr>(), list<name>(), tacs, ctx, full_ctx,
                                                                        j, ignore_failure, m_relax_main_opaque));
@@ -702,13 +706,13 @@ public:
         }
         if (!is_pi(f_type)) {
             // try coercion to function-class
-            optional<expr> c = get_coercion_to_fun(m_env, f_type);
+            optional<expr> c = get_coercion_to_fun(env(), f_type);
             if (c) {
                 f = mk_app(*c, f, f.get_tag());
                 f_type = infer_type(f);
                 lean_assert(is_pi(f_type));
             } else {
-                throw_kernel_exception(m_env, f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); });
+                throw_kernel_exception(env(), f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); });
             }
         }
         lean_assert(is_pi(f_type));
@@ -717,12 +721,12 @@ public:
 
     bool has_coercions_from(expr const & a_type) {
         expr const & a_cls = get_app_fn(whnf(a_type));
-        return is_constant(a_cls) && ::lean::has_coercions_from(m_env, const_name(a_cls));
+        return is_constant(a_cls) && ::lean::has_coercions_from(env(), const_name(a_cls));
     }
 
     bool has_coercions_to(expr const & d_type) {
         expr const & d_cls = get_app_fn(whnf(d_type));
-        return is_constant(d_cls) && ::lean::has_coercions_to(m_env, const_name(d_cls));
+        return is_constant(d_cls) && ::lean::has_coercions_to(env(), const_name(d_cls));
     }
 
     expr apply_coercion(expr const & a, expr a_type, expr d_type) {
@@ -730,7 +734,7 @@ public:
         d_type = whnf(d_type);
         expr const & d_cls = get_app_fn(d_type);
         if (is_constant(d_cls)) {
-            if (auto c = get_coercion(m_env, a_type, const_name(d_cls)))
+            if (auto c = get_coercion(env(), a_type, const_name(d_cls)))
                 return mk_app(*c, a, a.get_tag());
         }
         return a;
@@ -883,8 +887,8 @@ public:
 
     /** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */
     void save_info_data_core(expr const & e, expr const & r, bool replace) {
-        if (m_info_manager && m_pos_provider && (is_constant(e) || is_local(e) || is_placeholder(e))) {
-            if (auto p = m_pos_provider->get_pos_info(e)) {
+        if (infom() && pip() && (is_constant(e) || is_local(e) || is_placeholder(e))) {
+            if (auto p = pip()->get_pos_info(e)) {
                 type_checker::scope scope(*m_tc[m_relax_main_opaque]);
                 expr t = m_tc[m_relax_main_opaque]->infer(r);
                 if (replace) {
@@ -905,13 +909,13 @@ public:
     }
 
     expr visit_constant(expr const & e) {
-        declaration d = m_env.get(const_name(e));
+        declaration d = env().get(const_name(e));
         buffer<level> ls;
         for (level const & l : const_levels(e))
             ls.push_back(replace_univ_placeholder(l));
         unsigned num_univ_params = length(d.get_univ_params());
         if (num_univ_params < ls.size())
-            throw_kernel_exception(m_env, sstream() << "incorrect number of universe levels parameters for '"
+            throw_kernel_exception(env(), sstream() << "incorrect number of universe levels parameters for '"
                                    << const_name(e) << "', #" << num_univ_params
                                    << " expected, #" << ls.size() << " provided");
         // "fill" with meta universe parameters
@@ -939,10 +943,10 @@ public:
                 return e;
             }
         }
-        optional<expr> c = get_coercion_to_sort(m_env, t);
+        optional<expr> c = get_coercion_to_sort(env(), t);
         if (c)
             return mk_app(*c, e, e.get_tag());
-        throw_kernel_exception(m_env, e, [=](formatter const & fmt) { return pp_type_expected(fmt, e); });
+        throw_kernel_exception(env(), e, [=](formatter const & fmt) { return pp_type_expected(fmt, e); });
     }
 
     /** \brief Similar to instantiate_rev, but assumes that subst contains only local constants.
@@ -1061,7 +1065,7 @@ public:
         buffer<constraint> cs;
         cs.append(m_constraints);
         m_constraints.clear();
-        return unify(m_env, cs.size(), cs.data(), m_ngen.mk_child(), true, m_ios.get_options());
+        return unify(env(), cs.size(), cs.data(), m_ngen.mk_child(), true, ios().get_options());
     }
 
     static void collect_metavars(expr const & e, buffer<expr> & mvars) {
@@ -1078,9 +1082,9 @@ public:
         lean_assert(is_metavar(mvar));
         if (!m_displayed_errors.contains(mlocal_name(mvar))) {
             m_displayed_errors.insert(mlocal_name(mvar));
-            auto out = regular(m_env, m_ios);
+            auto out = regular(env(), ios());
             flycheck_error err(out);
-            display_error_pos(out, m_pos_provider, mvar);
+            display_error_pos(out, pip(), mvar);
             out << " unsolved placeholder, " << msg << "\n" << ps << endl;
         }
     }
@@ -1112,10 +1116,10 @@ public:
 
     optional<tactic> pre_tactic_to_tactic(expr const & pre_tac, expr const & mvar) {
         try {
-            return optional<tactic>(expr_to_tactic(m_env, pre_tac, m_pos_provider));
+            return optional<tactic>(expr_to_tactic(env(), pre_tac, pip()));
         } catch (expr_to_tactic_exception & ex) {
-            auto out = regular(m_env, m_ios);
-            display_error_pos(out, m_pos_provider, mvar);
+            auto out = regular(env(), ios());
+            display_error_pos(out, pip(), mvar);
             out << " " << ex.what();
             out << pp_indent_expr(out.get_formatter(), pre_tac) << endl << "failed at:"
                 << pp_indent_expr(out.get_formatter(), ex.get_expr()) << endl;
@@ -1140,7 +1144,7 @@ public:
         // make sure ps is a really a proof state for mvar.
         lean_assert(mlocal_name(get_app_fn(head(ps.get_goals()).get_meta())) == mlocal_name(mvar));
         try {
-            proof_state_seq seq = tac(m_env, m_ios, ps);
+            proof_state_seq seq = tac(env(), ios(), ps);
             auto r = seq.pull();
             if (!r) {
                 // tactic failed to produce any result
@@ -1157,8 +1161,8 @@ public:
                 return true;
             }
         } catch (tactic_exception & ex) {
-            auto out = regular(m_env, m_ios);
-            display_error_pos(out, m_pos_provider, ex.get_expr());
+            auto out = regular(env(), ios());
+            display_error_pos(out, pip(), ex.get_expr());
             out << " tactic failed: " << ex.what() << "\n";
             return false;
         }
@@ -1200,14 +1204,14 @@ public:
     }
 
     void display_unassigned_mvars(expr const & e, substitution const & s) {
-        if (m_check_unassigned && has_metavar(e)) {
+        if (check_unassigned() && has_metavar(e)) {
             substitution tmp_s(s);
             for_each(e, [&](expr const & e, unsigned) {
                     if (!is_metavar(e))
                         return has_metavar(e);
                     if (auto it = m_mvar2meta.find(mlocal_name(e))) {
                         expr meta      = tmp_s.instantiate(*it);
-                        expr meta_type = tmp_s.instantiate(type_checker(m_env).infer(meta));
+                        expr meta_type = tmp_s.instantiate(type_checker(env()).infer(meta));
                         goal g(meta, meta_type);
                         display_unsolved_proof_state(e, proof_state(goals(g), substitution(), m_ngen),
                                                      "don't know how to synthesize it");
@@ -1221,7 +1225,7 @@ public:
     expr apply(substitution & s, expr const & e, name_set & univ_params, buffer<name> & new_params) {
         expr r = s.instantiate(e);
         if (has_univ_metavar(r))
-            r = univ_metavars_to_params_fn(m_env, m_lls, s, univ_params, new_params)(r);
+            r = univ_metavars_to_params_fn(env(), lls(), s, univ_params, new_params)(r);
         r = solve_unassigned_mvars(s, r);
         display_unassigned_mvars(r, s);
         return r;
@@ -1235,15 +1239,15 @@ public:
     }
 
     void copy_info_to_manager(substitution s) {
-        if (!m_info_manager)
+        if (!infom())
             return;
         for (auto & p : m_pre_info_data)
             p = type_info_data(p.get_line(), p.get_column(), s.instantiate(p.get_type()));
-        m_info_manager->append(m_pre_info_data);
+        infom()->append(m_pre_info_data);
     }
 
     std::tuple<expr, level_param_names> operator()(expr const & e, bool _ensure_type, bool relax_main_opaque) {
-        flet<bool> set_relax(m_relax_main_opaque, relax_main_opaque && !get_hide_main_opaque(m_env));
+        flet<bool> set_relax(m_relax_main_opaque, relax_main_opaque && !get_hide_main_opaque(env()));
         expr r  = visit(e);
         if (_ensure_type)
             r = ensure_type(r);
@@ -1259,7 +1263,7 @@ public:
         lean_assert(!has_local(t)); lean_assert(!has_local(v));
         expr r_t      = ensure_type(visit(t));
         // Opaque definitions in the main module may treat other opaque definitions (in the main module) as transparent.
-        flet<bool> set_relax(m_relax_main_opaque, is_opaque && !get_hide_main_opaque(m_env));
+        flet<bool> set_relax(m_relax_main_opaque, is_opaque && !get_hide_main_opaque(env()));
         expr r_v      = visit(v);
         expr r_v_type = infer_type(r_v);
         justification j = mk_justification(r_v, [=](formatter const & fmt, substitution const & subst) {
@@ -1281,16 +1285,13 @@ public:
 
 static name g_tmp_prefix = name::mk_internal_unique_name();
 
-std::tuple<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, list<expr> const & ctx,
-                                              io_state const & ios, expr const & e, bool relax_main_opaque,
-                                              pos_info_provider * pp, bool check_unassigned, bool ensure_type,
-                                              info_manager * info) {
-    return elaborator(env, lls, ctx, ios, name_generator(g_tmp_prefix), pp, check_unassigned, info)(e, ensure_type, relax_main_opaque);
+std::tuple<expr, level_param_names> elaborate(elaborator_env & env, list<expr> const & ctx, expr const & e,
+                                              bool relax_main_opaque, bool ensure_type) {
+    return elaborator(env, ctx, name_generator(g_tmp_prefix))(e, ensure_type, relax_main_opaque);
 }
 
-std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios,
-                                                    name const & n, expr const & t, expr const & v, bool is_opaque, pos_info_provider * pp,
-                                                    info_manager * info) {
-    return elaborator(env, lls, list<expr>(), ios, name_generator(g_tmp_prefix), pp, true, info)(t, v, n, is_opaque);
+std::tuple<expr, expr, level_param_names> elaborate(elaborator_env & env, name const & n, expr const & t, expr const & v,
+                                                    bool is_opaque) {
+    return elaborator(env, list<expr>(), name_generator(g_tmp_prefix))(t, v, n, is_opaque);
 }
 }
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 742396d50..fd23d18f6 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -14,11 +14,26 @@ Author: Leonardo de Moura
 #include "frontends/lean/info_manager.h"
 
 namespace lean {
-std::tuple<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, list<expr> const & ctx,
-                                              io_state const & ios, expr const & e, bool relax_main_opaque,
-                                              pos_info_provider * pp = nullptr, bool check_unassigned = true,
-                                              bool ensure_type = false, info_manager * info = nullptr);
-std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls,
-                                                    io_state const & ios, name const & n, expr const & t, expr const & v,
-                                                    bool is_opaque, pos_info_provider * pp = nullptr, info_manager * info = nullptr);
+/** \brief Environment for elaboration, it contains all the information that is "scope-indenpendent" */
+class elaborator_env {
+    environment               m_env;
+    io_state                  m_ios;
+    local_decls<level>        m_lls; // local universe levels
+    pos_info_provider const * m_pos_provider;
+    info_manager *            m_info_manager;
+
+    // configuration
+    bool                      m_check_unassigned;
+    bool                      m_use_local_instances;
+    friend class elaborator;
+public:
+    elaborator_env(environment const & env, io_state const & ios, local_decls<level> const & lls,
+                   pos_info_provider const * pp = nullptr, info_manager * info = nullptr, bool check_unassigned = true);
+};
+
+std::tuple<expr, level_param_names> elaborate(elaborator_env & env, list<expr> const & ctx, expr const & e,
+                                              bool relax_main_opaque, bool ensure_type = false);
+
+std::tuple<expr, expr, level_param_names> elaborate(elaborator_env & env, name const & n, expr const & t, expr const & v,
+                                                    bool is_opaque);
 }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 12edf73a4..46b577f16 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -86,7 +86,6 @@ parser::parser(environment const & env, io_state const & ios,
     m_env(env), m_ios(ios), m_ngen(g_tmp_prefix),
     m_verbose(true), m_use_exceptions(use_exceptions),
     m_scanner(strm, strm_name, line), m_local_level_decls(lds), m_local_decls(eds),
-    m_pos_table(std::make_shared<pos_info_table>()),
     m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0),
     m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr) {
     m_num_threads = num_threads;
@@ -239,7 +238,9 @@ tag parser::get_tag(expr e) {
 }
 
 expr parser::save_pos(expr e, pos_info p) {
-    m_pos_table->insert(mk_pair(get_tag(e), p));
+    auto t = get_tag(e);
+    if (!m_pos_table.contains(t))
+        m_pos_table.insert(t, p);
     return e;
 }
 
@@ -302,11 +303,10 @@ expr parser::propagate_levels(expr const & e, levels const & ls) {
 }
 
 pos_info parser::pos_of(expr const & e, pos_info default_pos) {
-    auto it = m_pos_table->find(get_tag(e));
-    if (it == m_pos_table->end())
-        return default_pos;
+    if (auto it = m_pos_table.find(get_tag(e)))
+        return *it;
     else
-        return it->second;
+        return default_pos;
 }
 
 bool parser::curr_is_token(name const & tk) const {
@@ -517,39 +517,54 @@ level parser::parse_level(unsigned rbp) {
     return left;
 }
 
+elaborator_env parser::mk_elaborator_env(pos_info_provider const &  pp, bool check_unassigned) {
+    return elaborator_env(m_env, m_ios, m_local_level_decls, &pp, m_info_manager, check_unassigned);
+}
+
+elaborator_env parser::mk_elaborator_env(environment const & env, pos_info_provider const & pp) {
+    return elaborator_env(env, m_ios, m_local_level_decls, &pp, m_info_manager, true);
+}
+
+elaborator_env parser::mk_elaborator_env(environment const & env, local_level_decls const & lls, pos_info_provider const & pp) {
+    return elaborator_env(env, m_ios, lls, &pp, m_info_manager, true);
+}
+
 std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, list<expr> const & ctx) {
-    parser_pos_provider pp = get_pos_provider();
     bool relax            = true;
     bool check_unassigned = false;
     bool ensure_type      = false;
-    auto r = ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned, ensure_type,
-                               m_info_manager);
+    parser_pos_provider pp = get_pos_provider();
+    elaborator_env env = mk_elaborator_env(pp, check_unassigned);
+    auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
     m_pre_info_data.clear();
     return r;
 }
 
 std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<expr> const & ctx) {
-    parser_pos_provider pp = get_pos_provider();
     bool relax            = false;
     bool check_unassigned = true;
     bool ensure_type      = true;
-    auto r = ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned, ensure_type,
-                               m_info_manager);
+    parser_pos_provider pp = get_pos_provider();
+    elaborator_env env = mk_elaborator_env(pp, check_unassigned);
+    auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
     m_pre_info_data.clear();
     return r;
 }
 
 std::tuple<expr, level_param_names> parser::elaborate_at(environment const & env, expr const & e) {
-    parser_pos_provider pp = get_pos_provider();
     bool relax            = false;
-    auto r = ::lean::elaborate(env, m_local_level_decls, list<expr>(), m_ios, e, relax, &pp, m_info_manager);
+    parser_pos_provider pp = get_pos_provider();
+    elaborator_env eenv = mk_elaborator_env(env, pp);
+    auto r = ::lean::elaborate(eenv, list<expr>(), e, relax);
     m_pre_info_data.clear();
     return r;
 }
 
-std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name const & n, expr const & t, expr const & v, bool is_opaque) {
+std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name const & n, expr const & t, expr const & v,
+                                                                       bool is_opaque) {
     parser_pos_provider pp = get_pos_provider();
-    auto r = ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, is_opaque, &pp, m_info_manager);
+    elaborator_env eenv = mk_elaborator_env(pp);
+    auto r = ::lean::elaborate(eenv, n, t, v, is_opaque);
     m_pre_info_data.clear();
     return r;
 }
@@ -557,7 +572,8 @@ std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name cons
 std::tuple<expr, expr, level_param_names> parser::elaborate_definition_at(environment const & env, local_level_decls const & lls,
                                                                           name const & n, expr const & t, expr const & v, bool is_opaque) {
     parser_pos_provider pp = get_pos_provider();
-    auto r = ::lean::elaborate(env, lls, m_ios, n, t, v, is_opaque, &pp, m_info_manager);
+    elaborator_env eenv = mk_elaborator_env(env, lls, pp);
+    auto r = ::lean::elaborate(eenv, n, t, v, is_opaque);
     m_pre_info_data.clear();
     return r;
 }
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 91086a5ba..3d7317f68 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -22,6 +22,7 @@ Author: Leonardo de Moura
 #include "library/kernel_bindings.h"
 #include "library/definitions_cache.h"
 #include "frontends/lean/scanner.h"
+#include "frontends/lean/elaborator.h"
 #include "frontends/lean/local_decls.h"
 #include "frontends/lean/parser_config.h"
 #include "frontends/lean/parser_pos_provider.h"
@@ -75,7 +76,7 @@ class parser {
     unsigned                m_next_tag_idx;
     bool                    m_found_errors;
     bool                    m_used_sorry;
-    pos_info_table_ptr      m_pos_table;
+    pos_info_table          m_pos_table;
     // By default, when the parser finds a unknown identifier, it signs an error.
     // When the following flag is true, it creates a constant.
     // This flag is when we are trying to parse mutually recursive declarations.
@@ -162,6 +163,10 @@ class parser {
     void save_type_info(expr const & e);
     void save_pre_info_data();
 
+    elaborator_env mk_elaborator_env(pos_info_provider const & pp, bool check_unassigned = true);
+    elaborator_env mk_elaborator_env(environment const & env, pos_info_provider const & pp);
+    elaborator_env mk_elaborator_env(environment const & env, local_level_decls const & lls, pos_info_provider const & pp);
+
 public:
     parser(environment const & env, io_state const & ios,
            std::istream & strm, char const * str_name,
diff --git a/src/frontends/lean/parser_pos_provider.cpp b/src/frontends/lean/parser_pos_provider.cpp
index e2060bb0a..828eb20e5 100644
--- a/src/frontends/lean/parser_pos_provider.cpp
+++ b/src/frontends/lean/parser_pos_provider.cpp
@@ -9,22 +9,20 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser_pos_provider.h"
 
 namespace lean {
-parser_pos_provider::parser_pos_provider(pos_info_table_ptr const & pos_table,
-                                                   std::string const & strm_name, pos_info const & some_pos):
+parser_pos_provider::parser_pos_provider(pos_info_table const & pos_table,
+                                         std::string const & strm_name, pos_info const & some_pos):
     m_pos_table(pos_table), m_strm_name(strm_name), m_pos(some_pos) {}
 
 parser_pos_provider::~parser_pos_provider() {}
 
 optional<pos_info> parser_pos_provider::get_pos_info(expr const & e) const {
-    if (!m_pos_table)
-        return optional<pos_info>();
     tag t = e.get_tag();
     if (t == nulltag)
         return optional<pos_info>();
-    auto it = m_pos_table->find(t);
-    if (it == m_pos_table->end())
+    if (auto it = m_pos_table.find(t))
+        return optional<pos_info>(*it);
+    else
         return optional<pos_info>();
-    return optional<pos_info>(it->second);
 }
 
 pos_info parser_pos_provider::get_some_pos() const {
diff --git a/src/frontends/lean/parser_pos_provider.h b/src/frontends/lean/parser_pos_provider.h
index 95c7ff958..3d6a561a7 100644
--- a/src/frontends/lean/parser_pos_provider.h
+++ b/src/frontends/lean/parser_pos_provider.h
@@ -8,19 +8,18 @@ Author: Leonardo de Moura
 #include <string>
 #include <utility>
 #include <memory>
-#include <unordered_map>
+#include "util/rb_map.h"
 #include "kernel/pos_info_provider.h"
 
 namespace lean {
-typedef std::unordered_map<unsigned, pos_info> pos_info_table;
-typedef std::shared_ptr<pos_info_table> pos_info_table_ptr;
+typedef rb_map<unsigned, pos_info, unsigned_cmp> pos_info_table;
 
 class parser_pos_provider : public pos_info_provider {
-    pos_info_table_ptr m_pos_table;
-    std::string        m_strm_name;
-    pos_info           m_pos;
+    pos_info_table m_pos_table;
+    std::string    m_strm_name;
+    pos_info       m_pos;
 public:
-    parser_pos_provider(pos_info_table_ptr const & pos_table, std::string const & strm_name, pos_info const & some_pos);
+    parser_pos_provider(pos_info_table const & pos_table, std::string const & strm_name, pos_info const & some_pos);
     virtual ~parser_pos_provider();
     virtual optional<pos_info> get_pos_info(expr const & e) const;
     virtual pos_info get_some_pos() const;