diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index c31015d51..3ecc06919 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -45,6 +45,7 @@ Author: Leonardo de Moura
 #include "library/norm_num.h"
 #include "library/class_instance_resolution.h"
 #include "library/type_context.h"
+#include "library/tmp_type_context.h"
 
 namespace lean {
 void initialize_library_module() {
@@ -89,9 +90,11 @@ void initialize_library_module() {
     initialize_norm_num();
     initialize_class_instance_resolution();
     initialize_type_context();
+    initialize_tmp_type_context();
 }
 
 void finalize_library_module() {
+    finalize_tmp_type_context();
     finalize_type_context();
     finalize_class_instance_resolution();
     finalize_norm_num();
diff --git a/src/library/tmp_type_context.cpp b/src/library/tmp_type_context.cpp
index b525903de..ab030a80f 100644
--- a/src/library/tmp_type_context.cpp
+++ b/src/library/tmp_type_context.cpp
@@ -152,4 +152,12 @@ void tmp_type_context::commit() {
     lean_assert(!m_scopes.empty());
     m_scopes.pop_back();
 }
+
+void initialize_tmp_type_context() {
+    g_prefix = new name(name::mk_internal_unique_name());
+}
+
+void finalize_tmp_type_context() {
+    delete g_prefix;
+}
 }
diff --git a/src/library/tmp_type_context.h b/src/library/tmp_type_context.h
index 3dc210bfa..78c59e26e 100644
--- a/src/library/tmp_type_context.h
+++ b/src/library/tmp_type_context.h
@@ -80,5 +80,18 @@ public:
     virtual void push();
     virtual void pop();
     virtual void commit();
+
+    bool is_uvar_assigned(unsigned idx) const {
+        lean_assert(idx < m_uassignment.size());
+        return static_cast<bool>(m_uassignment[idx]);
+    }
+
+    bool is_mvar_assigned(unsigned idx) const {
+        lean_assert(idx < m_eassignment.size());
+        return static_cast<bool>(m_eassignment[idx]);
+    }
 };
+
+void initialize_tmp_type_context();
+void finalize_tmp_type_context();
 }