diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp
index 82bdb26ed7..7ef7c13785 100644
--- a/src/library/local_context.cpp
+++ b/src/library/local_context.cpp
@@ -107,6 +107,14 @@ void local_context::for_each_after(local_decl const & d, std::function<void(loca
     m_idx2local_decl.for_each_greater(d.get_idx(), [&](unsigned, local_decl const & d) { return fn(d); });
 }
 
+void local_context::pop_local_decl() {
+    lean_assert(!m_idx2local_decl.empty());
+    local_decl d = m_idx2local_decl.max();
+    lean_assert(!m_frozen_decls.contains(d.get_name()));
+    m_name2local_decl.erase(d.get_name());
+    m_idx2local_decl.erase(d.get_idx());
+}
+
 /* Return true iff all local_decl references in \c e are in \c s. */
 static bool locals_subset_of(expr const & e, name_set const & s) {
     bool ok = true;
diff --git a/src/library/local_context.h b/src/library/local_context.h
index 883edab581..05475fdd24 100644
--- a/src/library/local_context.h
+++ b/src/library/local_context.h
@@ -109,6 +109,8 @@ public:
     void freeze(name const & n);
     bool is_frozen(name const & n) const { return m_frozen_decls.contains(n); }
 
+    void pop_local_decl();
+
     /** \brief We say a local context is well-formed iff all local declarations only
         contain local_decl references that were defined before them.
 
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index a9cadc23b9..419849f30d 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -4,8 +4,33 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "util/flet.h"
 #include "library/type_context.h"
 
 namespace lean {
-
+expr type_context::relaxed_whnf(expr const & e) {
+    flet<transparency_mode> set(m_transparency_mode, transparency_mode::ALL);
+    return whnf(e);
+}
+
+bool type_context::relaxed_is_def_eq(expr const & e1, expr const & e2) {
+    flet<transparency_mode> set(m_transparency_mode, transparency_mode::ALL);
+    return is_def_eq(e1, e2);
+}
+
+name type_context::get_local_pp_name(expr const & e) const {
+    lean_assert(is_local(e));
+    if (is_local_decl_ref(e))
+        return m_lctx.get_local_decl(e)->get_name();
+    else
+        return local_pp_name(e);
+}
+
+expr type_context::push_local(name const & pp_name, expr const & type, binder_info const & bi) {
+    return m_lctx.mk_local_decl(pp_name, type, bi);
+}
+
+void type_context::pop_local() {
+    return m_lctx.pop_local_decl();
+}
 }
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 65680f79a9..cd6abec13e 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -139,6 +139,9 @@ class type_context : public abstract_type_context {
     tmp_trail          m_tmp_trail;
     /* Stack of backtracking point (aka scope) */
     scopes             m_scopes;
+
+    virtual bool on_is_def_eq_failure(expr const &, expr const &);
+
 public:
     type_context(metavar_context & mctx, local_context const & lctx, type_context_cache & cache,
                  transparency_mode m = transparency_mode::REDUCIBLE);
@@ -146,19 +149,26 @@ public:
                  transparency_mode m = transparency_mode::REDUCIBLE);
     virtual ~type_context();
 
-    virtual environment const & env() const;
-    virtual expr whnf(expr const & e);
-    virtual expr infer(expr const & e);
-    virtual expr check(expr const & e);
-    virtual bool is_def_eq(expr const & e1, expr const & e2);
+    virtual environment const & env() const override { return m_cache->m_env; }
 
-    virtual expr relaxed_whnf(expr const & e);
-    virtual bool relaxed_is_def_eq(expr const & e1, expr const & e2);
+    virtual expr whnf(expr const & e) override;
+    virtual expr infer(expr const & e) override;
+    virtual expr check(expr const & e) override;
+    virtual bool is_def_eq(expr const & e1, expr const & e2) override;
 
-    virtual optional<expr> is_stuck(expr const &);
-    virtual name get_local_pp_name(expr const & e) const;
+    virtual expr relaxed_whnf(expr const & e) override;
+    virtual bool relaxed_is_def_eq(expr const & e1, expr const & e2) override;
 
-    virtual bool on_is_def_eq_failure(expr const &, expr const &);
+    virtual optional<expr> is_stuck(expr const &) override;
+    virtual name get_local_pp_name(expr const & e) const override;
+
+    virtual expr push_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) override;
+    virtual void pop_local() override;
+    virtual expr abstract_locals(expr const & e, unsigned num_locals, expr const * locals) override;
+
+    expr push_let(name const & ppn, expr const & type, expr const & value) {
+        return m_lctx.mk_local_decl(ppn, type, value);
+    }
 
     bool is_prop(expr const & e);
 
diff --git a/src/util/rb_map.h b/src/util/rb_map.h
index 146e5b3626..418b580991 100644
--- a/src/util/rb_map.h
+++ b/src/util/rb_map.h
@@ -44,6 +44,9 @@ public:
         return r;
     }
 
+    T min() const { lean_assert(!empty()); return m_map.min()->second; }
+    T max() const { lean_assert(!empty()); return m_map.max()->second; }
+
     class ref {
         rb_map & m_map;
         K const &   m_key;