diff --git a/library/init/lean/elaborator/basic.lean b/library/init/lean/elaborator/basic.lean
index 92b379ca80..c8ff35117b 100644
--- a/library/init/lean/elaborator/basic.lean
+++ b/library/init/lean/elaborator/basic.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import init.control.reader
+import init.lean.metavarcontext
 import init.lean.namegenerator
 import init.lean.scopes
 import init.lean.parser.module
@@ -49,6 +50,7 @@ structure ElabState :=
 (messages : MessageLog := {})
 (cmdPos   : String.Pos := 0)
 (ngen     : NameGenerator := {})
+(mctx     : MetavarContext := {})
 (scopes   : List ElabScope := [{ cmd := "root", header := Name.anonymous }])
 
 inductive ElabException
diff --git a/library/init/lean/elaborator/preterm.lean b/library/init/lean/elaborator/preterm.lean
index 0dacabc8e9..dd1c877dda 100644
--- a/library/init/lean/elaborator/preterm.lean
+++ b/library/init/lean/elaborator/preterm.lean
@@ -10,6 +10,9 @@ namespace Lean
 
 abbrev PreTerm := Expr
 
+@[extern "lean_old_elaborate"]
+constant oldElaborate : Environment → Options → MetavarContext → LocalContext → PreTerm → Except (Option Position × Format) (Environment × MetavarContext × Expr) := default _
+
 abbrev PreTermElab := SyntaxNode → Elab PreTerm
 
 abbrev PreTermElabTable : Type := HashMap SyntaxNodeKind PreTermElab
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 6177f20f43..6ec3c2c138 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -3810,6 +3810,27 @@ elaborate(environment & env, options const & opts,
     return p;
 }
 
+extern "C" object * lean_old_elaborate(object * env, object * opts, object * mctx, object * lctx, object * p) {
+    try {
+        elaborator elab(environment(env), options(opts), metavar_context(mctx), local_context(lctx), false, false);
+        expr e = elab.elaborate(expr(p));
+        pair_ref<environment, pair_ref<metavar_context, expr>> r(elab.env(), pair_ref<metavar_context, expr>(elab.mctx(), e));
+        return mk_cnstr(1, r).steal();
+    } catch (elaborator_exception & ex) {
+        option_ref<object_ref> pos;
+        if (optional<pos_info> p = ex.get_pos()) {
+            pos = option_ref<object_ref>(mk_cnstr(0, box(p->first), box(p->second)));
+        }
+        return mk_cnstr(0, pair_ref<option_ref<object_ref>, format>(pos, ex.pp())).steal();
+    } catch (exception & ex) {
+        option_ref<object_ref> pos;
+        return mk_cnstr(0, pair_ref<option_ref<object_ref>, format>(pos, format(ex.what()))).steal();
+    } catch (...) {
+        option_ref<object_ref> pos;
+        return mk_cnstr(0, pair_ref<option_ref<object_ref>, format>(pos, format("internal error"))).steal();
+    }
+}
+
 void initialize_elaborator() {
     register_trace_class("elaborator");
     register_trace_class(name({"elaborator", "numeral"}));
diff --git a/src/kernel/local_ctx.h b/src/kernel/local_ctx.h
index 8da39cafb3..9f8d0117c3 100644
--- a/src/kernel/local_ctx.h
+++ b/src/kernel/local_ctx.h
@@ -54,6 +54,8 @@ protected:
     template<bool is_lambda> expr mk_binding(unsigned num, expr const * fvars, expr const & b) const;
 public:
     local_ctx();
+    explicit local_ctx(obj_arg o):object_ref(o) {}
+    local_ctx(b_obj_arg o, bool):object_ref(o, true) {}
     local_ctx(local_ctx const & other):object_ref(other) {}
     local_ctx(local_ctx && other):object_ref(other) {}
     local_ctx & operator=(local_ctx const & other) { object_ref::operator=(other); return *this; }
diff --git a/src/library/local_context.h b/src/library/local_context.h
index 85a376c3cb..70d7ffda98 100644
--- a/src/library/local_context.h
+++ b/src/library/local_context.h
@@ -49,6 +49,8 @@ class local_context : public local_ctx {
     optional<local_decl> get_decl_at(unsigned idx) const;
 public:
     local_context() {}
+    explicit local_context(obj_arg o):local_ctx(o) {}
+    local_context(b_obj_arg o, bool):local_ctx(o, true) {}
 
     expr mk_local_decl(expr const & type, binder_info bi = mk_binder_info());
     expr mk_local_decl(expr const & type, expr const & value);
diff --git a/src/library/metavar_context.h b/src/library/metavar_context.h
index 4818452fd9..ed32077f0d 100644
--- a/src/library/metavar_context.h
+++ b/src/library/metavar_context.h
@@ -48,6 +48,8 @@ class metavar_context : public object_ref {
     friend struct interface_impl;
 public:
     metavar_context();
+    explicit metavar_context(obj_arg o):object_ref(o) {}
+    metavar_context(b_obj_arg o, bool):object_ref(o, true) {}
     metavar_context(metavar_context const & other):object_ref(other) {}
     metavar_context(metavar_context && other):object_ref(other) {}
     metavar_context & operator=(metavar_context const & other) { object_ref::operator=(other); return *this; }
diff --git a/src/util/options.h b/src/util/options.h
index 5ae29b34b7..19cc8f1de8 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -16,6 +16,7 @@ class options {
     options(kvmap const & v):m_value(v) {}
 public:
     options() {}
+    explicit options(obj_arg o):m_value(o) {}
     options(b_obj_arg o, bool v):m_value(o, v) {}
     options(options const & o):m_value(o.m_value) {}
     options(options && o):m_value(std::move(o.m_value)) {}