diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp
index 706033632..51da33d80 100644
--- a/src/kernel/free_vars.cpp
+++ b/src/kernel/free_vars.cpp
@@ -111,7 +111,7 @@ bool has_free_vars(expr const & e) {
 */
 class free_var_range_fn {
     expr_map<unsigned>  m_cached;
-    optional<metavar_env> const & m_menv;
+    optional<ro_metavar_env> const & m_menv;
 
     static unsigned dec(unsigned s) { return (s == 0) ? 0 : s - 1; }
 
@@ -215,19 +215,19 @@ class free_var_range_fn {
         return result;
     }
 public:
-    free_var_range_fn(optional<metavar_env> const & menv):m_menv(menv) {}
+    free_var_range_fn(optional<ro_metavar_env> const & menv):m_menv(menv) {}
     unsigned operator()(expr const & e) { return apply(e); }
 };
 
-unsigned free_var_range(expr const & e, metavar_env const & menv) {
+unsigned free_var_range(expr const & e, ro_metavar_env const & menv) {
     if (closed(e))
         return 0;
     else
-        return free_var_range_fn(some_menv(menv))(e);
+        return free_var_range_fn(some_ro_menv(menv))(e);
 }
 
 unsigned free_var_range(expr const & e) {
-    return free_var_range_fn(none_menv())(e);
+    return free_var_range_fn(none_ro_menv())(e);
 }
 
 /**
@@ -338,7 +338,7 @@ protected:
         return result;
     }
 public:
-    has_free_var_in_range_fn(unsigned low, unsigned high, optional<metavar_env> const & menv):
+    has_free_var_in_range_fn(unsigned low, unsigned high, optional<ro_metavar_env> const & menv):
         m_low(low),
         m_high(high) {
         lean_assert(low < high);
@@ -348,16 +348,16 @@ public:
     bool operator()(expr const & e) { return apply(e, 0); }
 };
 
-bool has_free_var(expr const & e, unsigned low, unsigned high, optional<metavar_env> const & menv) {
+bool has_free_var(expr const & e, unsigned low, unsigned high, optional<ro_metavar_env> const & menv) {
     return high > low && !closed(e) && has_free_var_in_range_fn(low, high, menv)(e);
 }
-bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const & menv) { return has_free_var(e, low, high, some_menv(menv)); }
-bool has_free_var(expr const & e, unsigned low, unsigned high) { return has_free_var(e, low, high, none_menv()); }
-bool has_free_var(expr const & e, unsigned i, optional<metavar_env> const & menv) { return has_free_var(e, i, i+1, menv); }
-bool has_free_var(expr const & e, unsigned i, metavar_env const & menv) { return has_free_var(e, i, i+1, menv); }
+bool has_free_var(expr const & e, unsigned low, unsigned high, ro_metavar_env const & menv) { return has_free_var(e, low, high, some_ro_menv(menv)); }
+bool has_free_var(expr const & e, unsigned low, unsigned high) { return has_free_var(e, low, high, none_ro_menv()); }
+bool has_free_var(expr const & e, unsigned i, optional<ro_metavar_env> const & menv) { return has_free_var(e, i, i+1, menv); }
+bool has_free_var(expr const & e, unsigned i, ro_metavar_env const & menv) { return has_free_var(e, i, i+1, menv); }
 bool has_free_var(expr const & e, unsigned i) { return has_free_var(e, i, i+1); }
 
-bool has_free_var(context_entry const & e, unsigned low, unsigned high, metavar_env const & menv) {
+bool has_free_var(context_entry const & e, unsigned low, unsigned high, ro_metavar_env const & menv) {
     if (high <= low)
         return false;
     auto d = e.get_domain();
@@ -365,10 +365,10 @@ bool has_free_var(context_entry const & e, unsigned low, unsigned high, metavar_
     return (d && has_free_var(*d, low, high, menv)) || (b && has_free_var(*b, low, high, menv));
 }
 
-bool has_free_var_ge(expr const & e, unsigned low, metavar_env const & menv) { return has_free_var(e, low, std::numeric_limits<unsigned>::max(), menv); }
+bool has_free_var_ge(expr const & e, unsigned low, ro_metavar_env const & menv) { return has_free_var(e, low, std::numeric_limits<unsigned>::max(), menv); }
 bool has_free_var_ge(expr const & e, unsigned low) { return has_free_var(e, low, std::numeric_limits<unsigned>::max()); }
 
-expr lower_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env> const & DEBUG_CODE(menv)) {
+expr lower_free_vars(expr const & e, unsigned s, unsigned d, optional<ro_metavar_env> const & DEBUG_CODE(menv)) {
     if (d == 0 || closed(e))
         return e;
     lean_assert(s >= d);
@@ -382,13 +382,13 @@ expr lower_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_en
             }
         });
 }
-expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv) { return lower_free_vars(e, s, d, some_menv(menv)); }
-expr lower_free_vars(expr const & e, unsigned s, unsigned d) { return lower_free_vars(e, s, d, none_menv()); }
-expr lower_free_vars(expr const & e, unsigned d, optional<metavar_env> const & menv) { return lower_free_vars(e, d, d, menv); }
-expr lower_free_vars(expr const & e, unsigned d, metavar_env const & menv) { return lower_free_vars(e, d, d, menv); }
+expr lower_free_vars(expr const & e, unsigned s, unsigned d, ro_metavar_env const & menv) { return lower_free_vars(e, s, d, some_ro_menv(menv)); }
+expr lower_free_vars(expr const & e, unsigned s, unsigned d) { return lower_free_vars(e, s, d, none_ro_menv()); }
+expr lower_free_vars(expr const & e, unsigned d, optional<ro_metavar_env> const & menv) { return lower_free_vars(e, d, d, menv); }
+expr lower_free_vars(expr const & e, unsigned d, ro_metavar_env const & menv) { return lower_free_vars(e, d, d, menv); }
 expr lower_free_vars(expr const & e, unsigned d) { return lower_free_vars(e, d, d); }
 
-context_entry lower_free_vars(context_entry const & e, unsigned s, unsigned d, metavar_env const & menv) {
+context_entry lower_free_vars(context_entry const & e, unsigned s, unsigned d, ro_metavar_env const & menv) {
     auto domain = e.get_domain();
     auto body   = e.get_body();
     if (domain && body)
@@ -399,7 +399,7 @@ context_entry lower_free_vars(context_entry const & e, unsigned s, unsigned d, m
         return context_entry(e.get_name(), none_expr(), lower_free_vars(*body, s, d, menv));
 }
 
-expr lift_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env> const & menv) {
+expr lift_free_vars(expr const & e, unsigned s, unsigned d, optional<ro_metavar_env> const & menv) {
     if (d == 0 || closed(e))
         return e;
     return replace(e, [=](expr const & e, unsigned offset) -> expr {
@@ -412,13 +412,13 @@ expr lift_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env
             }
         });
 }
-expr lift_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv) { return lift_free_vars(e, s, d, some_menv(menv)); }
-expr lift_free_vars(expr const & e, unsigned s, unsigned d) { return lift_free_vars(e, s, d, none_menv()); }
-expr lift_free_vars(expr const & e, unsigned d, optional<metavar_env> const & menv) { return lift_free_vars(e, 0, d, menv); }
+expr lift_free_vars(expr const & e, unsigned s, unsigned d, ro_metavar_env const & menv) { return lift_free_vars(e, s, d, some_ro_menv(menv)); }
+expr lift_free_vars(expr const & e, unsigned s, unsigned d) { return lift_free_vars(e, s, d, none_ro_menv()); }
+expr lift_free_vars(expr const & e, unsigned d, optional<ro_metavar_env> const & menv) { return lift_free_vars(e, 0, d, menv); }
 expr lift_free_vars(expr const & e, unsigned d) { return lift_free_vars(e, 0, d); }
-expr lift_free_vars(expr const & e, unsigned d, metavar_env const & menv) { return lift_free_vars(e, 0, d, menv); }
+expr lift_free_vars(expr const & e, unsigned d, ro_metavar_env const & menv) { return lift_free_vars(e, 0, d, menv); }
 
-context_entry lift_free_vars(context_entry const & e, unsigned s, unsigned d, metavar_env const & menv) {
+context_entry lift_free_vars(context_entry const & e, unsigned s, unsigned d, ro_metavar_env const & menv) {
     auto domain = e.get_domain();
     auto body   = e.get_body();
     if (domain && body)
diff --git a/src/kernel/free_vars.h b/src/kernel/free_vars.h
index 6c12f1aff..2c8c537a5 100644
--- a/src/kernel/free_vars.h
+++ b/src/kernel/free_vars.h
@@ -35,7 +35,7 @@ class metavar_env;
    [inst:s v] R  ===>  if s >= R then R else max(R-1, range_of(v))
    [lift:s:n] R  ===>  if s >= R then R else R + n
 */
-unsigned free_var_range(expr const & e, metavar_env const & menv);
+unsigned free_var_range(expr const & e, ro_metavar_env const & menv);
 unsigned free_var_range(expr const & e);
 
 /**
@@ -45,17 +45,17 @@ unsigned free_var_range(expr const & e);
     \remark If menv is not none, then we use \c free_var_range to compute the free variables that may
     occur in a metavariable.
 */
-bool has_free_var(expr const & e, unsigned low, unsigned high, optional<metavar_env> const & menv);
-bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const & menv);
+bool has_free_var(expr const & e, unsigned low, unsigned high, optional<ro_metavar_env> const & menv);
+bool has_free_var(expr const & e, unsigned low, unsigned high, ro_metavar_env const & menv);
 bool has_free_var(expr const & e, unsigned low, unsigned high);
 /**
     \brief Return true iff \c e contains the free variable <tt>(var i)</tt>.
 */
-bool has_free_var(expr const & e, unsigned i, optional<metavar_env> const & menv);
-bool has_free_var(expr const & e, unsigned i, metavar_env const & menv);
+bool has_free_var(expr const & e, unsigned i, optional<ro_metavar_env> const & menv);
+bool has_free_var(expr const & e, unsigned i, ro_metavar_env const & menv);
 bool has_free_var(expr const & e, unsigned i);
 
-bool has_free_var(context_entry const & e, unsigned low, unsigned high, metavar_env const & menv);
+bool has_free_var(context_entry const & e, unsigned low, unsigned high, ro_metavar_env const & menv);
 
 /**
    \brief Return true iff \c e contains a free variable >= low.
@@ -63,7 +63,7 @@ bool has_free_var(context_entry const & e, unsigned low, unsigned high, metavar_
    \remark If menv is provided, then we use \c free_var_range to compute the free variables that may
     occur in a metavariable.
 */
-bool has_free_var_ge(expr const & e, unsigned low, metavar_env const & menv);
+bool has_free_var_ge(expr const & e, unsigned low, ro_metavar_env const & menv);
 bool has_free_var_ge(expr const & e, unsigned low);
 
 /**
@@ -75,14 +75,14 @@ bool has_free_var_ge(expr const & e, unsigned low);
 
    \remark The parameter menv is only used for debugging purposes
 */
-expr lower_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env> const & menv);
-expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv);
+expr lower_free_vars(expr const & e, unsigned s, unsigned d, optional<ro_metavar_env> const & menv);
+expr lower_free_vars(expr const & e, unsigned s, unsigned d, ro_metavar_env const & menv);
 expr lower_free_vars(expr const & e, unsigned s, unsigned d);
-expr lower_free_vars(expr const & e, unsigned d, optional<metavar_env> const & menv);
-expr lower_free_vars(expr const & e, unsigned d, metavar_env const & menv);
+expr lower_free_vars(expr const & e, unsigned d, optional<ro_metavar_env> const & menv);
+expr lower_free_vars(expr const & e, unsigned d, ro_metavar_env const & menv);
 expr lower_free_vars(expr const & e, unsigned d);
 
-context_entry lower_free_vars(context_entry const & e, unsigned s, unsigned d, metavar_env const & menv);
+context_entry lower_free_vars(context_entry const & e, unsigned s, unsigned d, ro_metavar_env const & menv);
 
 /**
    \brief Lift free variables >= s in \c e by d.
@@ -90,12 +90,12 @@ context_entry lower_free_vars(context_entry const & e, unsigned s, unsigned d, m
    \remark When the parameter menv is not none, this function will minimize the use
    of the local entry lift in metavariables occurring in \c e.
 */
-expr lift_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env> const & menv);
+expr lift_free_vars(expr const & e, unsigned s, unsigned d, optional<ro_metavar_env> const & menv);
 expr lift_free_vars(expr const & e, unsigned s, unsigned d);
-expr lift_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv);
-expr lift_free_vars(expr const & e, unsigned d, optional<metavar_env> const & menv);
-expr lift_free_vars(expr const & e, unsigned d, metavar_env const & menv);
+expr lift_free_vars(expr const & e, unsigned s, unsigned d, ro_metavar_env const & menv);
+expr lift_free_vars(expr const & e, unsigned d, optional<ro_metavar_env> const & menv);
+expr lift_free_vars(expr const & e, unsigned d, ro_metavar_env const & menv);
 expr lift_free_vars(expr const & e, unsigned d);
 
-context_entry lift_free_vars(context_entry const & e, unsigned s, unsigned d, metavar_env const & menv);
+context_entry lift_free_vars(context_entry const & e, unsigned s, unsigned d, ro_metavar_env const & menv);
 }
diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp
index 2f9586bac..ec2d3754e 100644
--- a/src/kernel/instantiate.cpp
+++ b/src/kernel/instantiate.cpp
@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 template<bool ClosedSubst>
-expr instantiate_core(expr const & a, unsigned s, unsigned n, expr const * subst, optional<metavar_env> const & menv) {
+expr instantiate_core(expr const & a, unsigned s, unsigned n, expr const * subst, optional<ro_metavar_env> const & menv) {
     return replace(a, [=](expr const & m, unsigned offset) -> expr {
             if (is_var(m)) {
                 unsigned vidx = var_idx(m);
@@ -42,36 +42,36 @@ expr instantiate_core(expr const & a, unsigned s, unsigned n, expr const * subst
         });
 }
 
-expr instantiate_with_closed(expr const & a, unsigned n, expr const * s, optional<metavar_env> const & menv) {
+expr instantiate_with_closed(expr const & a, unsigned n, expr const * s, optional<ro_metavar_env> const & menv) {
     lean_assert(std::all_of(s, s+n, [&](expr const & e) { return !has_free_var(e, 0, std::numeric_limits<unsigned>::max(), menv); }));
     return instantiate_core<true>(a, 0, n, s, menv);
 }
-expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, metavar_env const & menv) { return instantiate_with_closed(e, n, s, some_menv(menv)); }
-expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) { return instantiate_with_closed(e, n, s, none_menv()); }
+expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv) { return instantiate_with_closed(e, n, s, some_ro_menv(menv)); }
+expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) { return instantiate_with_closed(e, n, s, none_ro_menv()); }
 expr instantiate_with_closed(expr const & e, std::initializer_list<expr> const & l) { return instantiate_with_closed(e, l.size(), l.begin()); }
-expr instantiate_with_closed(expr const & e, expr const & s, optional<metavar_env> const & menv) { return instantiate_with_closed(e, 1, &s, menv); }
+expr instantiate_with_closed(expr const & e, expr const & s, optional<ro_metavar_env> const & menv) { return instantiate_with_closed(e, 1, &s, menv); }
 expr instantiate_with_closed(expr const & e, expr const & s) { return instantiate_with_closed(e, 1, &s); }
-expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const & menv) { return instantiate_with_closed(e, s, some_menv(menv)); }
+expr instantiate_with_closed(expr const & e, expr const & s, ro_metavar_env const & menv) { return instantiate_with_closed(e, s, some_ro_menv(menv)); }
 
-expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, optional<metavar_env> const & menv) {
+expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, optional<ro_metavar_env> const & menv) {
     return instantiate_core<false>(a, s, n, subst, menv);
 }
-expr instantiate(expr const & e, unsigned n, expr const * s, optional<metavar_env> const & menv) { return instantiate(e, 0, n, s, menv); }
-expr instantiate(expr const & e, unsigned n, expr const * s, metavar_env const & menv) { return instantiate(e, n, s, some_menv(menv)); }
-expr instantiate(expr const & e, unsigned n, expr const * s) { return instantiate(e, n, s, none_menv()); }
+expr instantiate(expr const & e, unsigned n, expr const * s, optional<ro_metavar_env> const & menv) { return instantiate(e, 0, n, s, menv); }
+expr instantiate(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv) { return instantiate(e, n, s, some_ro_menv(menv)); }
+expr instantiate(expr const & e, unsigned n, expr const * s) { return instantiate(e, n, s, none_ro_menv()); }
 expr instantiate(expr const & e, std::initializer_list<expr> const & l) {  return instantiate(e, l.size(), l.begin()); }
-expr instantiate(expr const & e, unsigned i, expr const & s, optional<metavar_env> const & menv) { return instantiate(e, i, 1, &s, menv); }
-expr instantiate(expr const & e, unsigned i, expr const & s, metavar_env const & menv) { return instantiate(e, i, 1, &s, some_menv(menv)); }
-expr instantiate(expr const & e, unsigned i, expr const & s) { return instantiate(e, i, 1, &s, none_menv()); }
-expr instantiate(expr const & e, expr const & s, optional<metavar_env> const & menv) { return instantiate(e, 1, &s, menv); }
-expr instantiate(expr const & e, expr const & s, metavar_env const & menv) { return instantiate(e, s, some_menv(menv)); }
-expr instantiate(expr const & e, expr const & s) { return instantiate(e, s, none_menv()); }
+expr instantiate(expr const & e, unsigned i, expr const & s, optional<ro_metavar_env> const & menv) { return instantiate(e, i, 1, &s, menv); }
+expr instantiate(expr const & e, unsigned i, expr const & s, ro_metavar_env const & menv) { return instantiate(e, i, 1, &s, some_ro_menv(menv)); }
+expr instantiate(expr const & e, unsigned i, expr const & s) { return instantiate(e, i, 1, &s, none_ro_menv()); }
+expr instantiate(expr const & e, expr const & s, optional<ro_metavar_env> const & menv) { return instantiate(e, 1, &s, menv); }
+expr instantiate(expr const & e, expr const & s, ro_metavar_env const & menv) { return instantiate(e, s, some_ro_menv(menv)); }
+expr instantiate(expr const & e, expr const & s) { return instantiate(e, s, none_ro_menv()); }
 
 bool is_head_beta(expr const & t) {
     return is_app(t) && is_lambda(arg(t, 0));
 }
 
-expr apply_beta(expr f, unsigned num_args, expr const * args, optional<metavar_env> const & menv) {
+expr apply_beta(expr f, unsigned num_args, expr const * args, optional<ro_metavar_env> const & menv) {
     if (!is_lambda(f)) {
         buffer<expr> new_args;
         new_args.push_back(f);
@@ -96,20 +96,20 @@ expr apply_beta(expr f, unsigned num_args, expr const * args, optional<metavar_e
         }
     }
 }
-expr apply_beta(expr f, unsigned num_args, expr const * args, metavar_env const & menv) { return apply_beta(f, num_args, args, some_menv(menv)); }
-expr apply_beta(expr f, unsigned num_args, expr const * args) { return apply_beta(f, num_args, args, none_menv()); }
+expr apply_beta(expr f, unsigned num_args, expr const * args, ro_metavar_env const & menv) { return apply_beta(f, num_args, args, some_ro_menv(menv)); }
+expr apply_beta(expr f, unsigned num_args, expr const * args) { return apply_beta(f, num_args, args, none_ro_menv()); }
 
-expr head_beta_reduce(expr const & t, optional<metavar_env> const & menv) {
+expr head_beta_reduce(expr const & t, optional<ro_metavar_env> const & menv) {
     if (!is_head_beta(t)) {
         return t;
     } else {
         return apply_beta(arg(t, 0), num_args(t) - 1, &arg(t, 1), menv);
     }
 }
-expr head_beta_reduce(expr const & t) { return head_beta_reduce(t, none_menv()); }
-expr head_beta_reduce(expr const & t, metavar_env const & menv) { return head_beta_reduce(t, some_menv(menv)); }
+expr head_beta_reduce(expr const & t) { return head_beta_reduce(t, none_ro_menv()); }
+expr head_beta_reduce(expr const & t, ro_metavar_env const & menv) { return head_beta_reduce(t, some_ro_menv(menv)); }
 
-expr beta_reduce(expr t, optional<metavar_env> const & menv) {
+expr beta_reduce(expr t, optional<ro_metavar_env> const & menv) {
     auto f = [=](expr const & m, unsigned) -> expr {
         if (is_head_beta(m))
             return head_beta_reduce(m, menv);
@@ -124,6 +124,6 @@ expr beta_reduce(expr t, optional<metavar_env> const & menv) {
             t = new_t;
     }
 }
-expr beta_reduce(expr t, metavar_env const & menv) { return beta_reduce(t, some_menv(menv)); }
-expr beta_reduce(expr t) { return beta_reduce(t, none_menv()); }
+expr beta_reduce(expr t, ro_metavar_env const & menv) { return beta_reduce(t, some_ro_menv(menv)); }
+expr beta_reduce(expr t) { return beta_reduce(t, none_ro_menv()); }
 }
diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h
index a5328eee2..c9952f539 100644
--- a/src/kernel/instantiate.h
+++ b/src/kernel/instantiate.h
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 
 namespace lean {
-class metavar_env;
+class ro_metavar_env;
 /**
    \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e.
 
@@ -17,12 +17,12 @@ class metavar_env;
    \remark When the parameter menv is not none, this function will minimize the use
    of the local entry inst in metavariables occurring in \c e.
 */
-expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, optional<metavar_env> const & menv);
-expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, metavar_env const & menv);
+expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, optional<ro_metavar_env> const & menv);
+expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv);
 expr instantiate_with_closed(expr const & e, unsigned n, expr const * s);
 expr instantiate_with_closed(expr const & e, std::initializer_list<expr> const & l);
-expr instantiate_with_closed(expr const & e, expr const & s, optional<metavar_env> const & menv);
-expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const & menv);
+expr instantiate_with_closed(expr const & e, expr const & s, optional<ro_metavar_env> const & menv);
+expr instantiate_with_closed(expr const & e, expr const & s, ro_metavar_env const & menv);
 expr instantiate_with_closed(expr const & e, expr const & s);
 
 /**
@@ -31,34 +31,34 @@ expr instantiate_with_closed(expr const & e, expr const & s);
    \remark When the parameter menv is not none, this function will minimize the use
    of the local entry inst in metavariables occurring in \c e.
 */
-expr instantiate(expr const & e, unsigned n, expr const * s, optional<metavar_env> const & menv);
-expr instantiate(expr const & e, unsigned n, expr const * s, metavar_env const & menv);
+expr instantiate(expr const & e, unsigned n, expr const * s, optional<ro_metavar_env> const & menv);
+expr instantiate(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv);
 expr instantiate(expr const & e, unsigned n, expr const * s);
 expr instantiate(expr const & e, std::initializer_list<expr> const & l);
 /**
    \brief Replace free variable \c i with \c s in \c e.
 */
-expr instantiate(expr const & e, unsigned i, expr const & s, optional<metavar_env> const & menv);
-expr instantiate(expr const & e, unsigned i, expr const & s, metavar_env const & menv);
+expr instantiate(expr const & e, unsigned i, expr const & s, optional<ro_metavar_env> const & menv);
+expr instantiate(expr const & e, unsigned i, expr const & s, ro_metavar_env const & menv);
 expr instantiate(expr const & e, unsigned i, expr const & s);
 /**
    \brief Replace free variable \c 0 with \c s in \c e.
 */
-expr instantiate(expr const & e, expr const & s, optional<metavar_env> const & menv);
-expr instantiate(expr const & e, expr const & s, metavar_env const & menv);
+expr instantiate(expr const & e, expr const & s, optional<ro_metavar_env> const & menv);
+expr instantiate(expr const & e, expr const & s, ro_metavar_env const & menv);
 expr instantiate(expr const & e, expr const & s);
 
-expr apply_beta(expr f, unsigned num_args, expr const * args, optional<metavar_env> const & menv);
-expr apply_beta(expr f, unsigned num_args, expr const * args, metavar_env const & menv);
+expr apply_beta(expr f, unsigned num_args, expr const * args, optional<ro_metavar_env> const & menv);
+expr apply_beta(expr f, unsigned num_args, expr const * args, ro_metavar_env const & menv);
 expr apply_beta(expr f, unsigned num_args, expr const * args);
 
 bool is_head_beta(expr const & t);
 
-expr head_beta_reduce(expr const & t, optional<metavar_env> const & menv);
-expr head_beta_reduce(expr const & t, metavar_env const & menv);
+expr head_beta_reduce(expr const & t, optional<ro_metavar_env> const & menv);
+expr head_beta_reduce(expr const & t, ro_metavar_env const & menv);
 expr head_beta_reduce(expr const & t);
 
-expr beta_reduce(expr t, optional<metavar_env> const & menv);
-expr beta_reduce(expr t, metavar_env const & menv);
+expr beta_reduce(expr t, optional<ro_metavar_env> const & menv);
+expr beta_reduce(expr t, ro_metavar_env const & menv);
 expr beta_reduce(expr t);
 }
diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index b58bd84cd..ad7edea6d 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -224,7 +224,7 @@ bool metavar_env_cell::assign(expr const & m, expr const & t) {
     return assign(m, t, j);
 }
 
-expr apply_local_context(expr const & a, local_context const & lctx, optional<metavar_env> const & menv) {
+expr apply_local_context(expr const & a, local_context const & lctx, optional<ro_metavar_env> const & menv) {
     if (lctx) {
         if (is_metavar(a)) {
             return mk_metavar(metavar_name(a), append(lctx, metavar_lctx(a)));
@@ -463,7 +463,7 @@ local_context add_lift(local_context const & lctx, unsigned s, unsigned n) {
     return cons(mk_lift(s, n), lctx);
 }
 
-expr add_lift(expr const & m, unsigned s, unsigned n, optional<metavar_env> const & menv) {
+expr add_lift(expr const & m, unsigned s, unsigned n, optional<ro_metavar_env> const & menv) {
     if (menv && s >= free_var_range(m, *menv))
         return m;
     return update_metavar(m, add_lift(metavar_lctx(m), s, n));
@@ -487,7 +487,7 @@ local_context add_inst(local_context const & lctx, unsigned s, expr const & v) {
     return cons(mk_inst(s, v), lctx);
 }
 
-expr add_inst(expr const & m, unsigned s, expr const & v, optional<metavar_env> const & menv) {
+expr add_inst(expr const & m, unsigned s, expr const & v, optional<ro_metavar_env> const & menv) {
     if (menv && s >= free_var_range(m, *menv))
         return m;
     return update_metavar(m, add_inst(metavar_lctx(m), s, v));
diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h
index d226e360d..fd5fa5970 100644
--- a/src/kernel/metavar.h
+++ b/src/kernel/metavar.h
@@ -246,8 +246,10 @@ inline context instantiate_metavars(optional<metavar_env> const & menv, context
    \brief Read-only reference to metavariable environment (cell).
 */
 class ro_metavar_env {
+    friend class optional<ro_metavar_env>;
     friend class metavar_env;
     metavar_env_cell * m_ptr;
+    explicit ro_metavar_env(metavar_env_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
 public:
     ro_metavar_env():m_ptr(new metavar_env_cell()) { m_ptr->inc_ref(); }
     ro_metavar_env(metavar_env const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
@@ -259,8 +261,16 @@ public:
     metavar_env_cell const * operator->() const { return m_ptr; }
     metavar_env_cell const & operator*() const { return *m_ptr; }
     metavar_env copy() const { return metavar_env(new metavar_env_cell(*m_ptr)); }
+    friend bool is_eqp(ro_metavar_env const & menv1, ro_metavar_env const & menv2) { return menv1.m_ptr == menv2.m_ptr; }
+    friend bool operator==(ro_metavar_env const & menv1, ro_metavar_env const & menv2) { return is_eqp(menv1, menv2); }
 };
 
+SPECIALIZE_OPTIONAL_FOR_SMART_PTR(ro_metavar_env)
+inline optional<ro_metavar_env> none_ro_menv() { return optional<ro_metavar_env>(); }
+inline optional<ro_metavar_env> some_ro_menv(ro_metavar_env const & e) { return optional<ro_metavar_env>(e); }
+inline optional<ro_metavar_env> some_ro_menv(ro_metavar_env && e) { return optional<ro_metavar_env>(std::forward<ro_metavar_env>(e)); }
+inline optional<ro_metavar_env> const & to_ro_menv(optional<metavar_env> const & menv) { return reinterpret_cast<optional<ro_metavar_env> const &>(menv); }
+
 /**
    \brief A cached weak reference to a metavariable environment + timestamp at the time of
    the caching. This object may also cache optional references.
@@ -280,6 +290,7 @@ public:
     bool update(metavar_env const & menv) { return update(some(menv)); }
     explicit operator bool() const { return static_cast<bool>(m_menv); }
     optional<metavar_env> const & to_some_menv() const { return m_menv; }
+    optional<ro_metavar_env> const & to_some_ro_menv() const { return to_ro_menv(m_menv); }
     metavar_env operator*() const { return *m_menv; }
     metavar_env_cell * operator->() const { lean_assert(m_menv); return (*m_menv).operator->(); }
 };
@@ -287,9 +298,9 @@ public:
 /**
    \brief Apply the changes in \c lctx to \c a.
 */
-expr apply_local_context(expr const & a, local_context const & lctx, optional<metavar_env> const & menv);
-inline expr apply_local_context(expr const & a, local_context const & lctx, metavar_env const & menv) { return apply_local_context(a, lctx, some_menv(menv)); }
-inline expr apply_local_context(expr const & a, local_context const & lctx) { return apply_local_context(a, lctx, none_menv()); }
+expr apply_local_context(expr const & a, local_context const & lctx, optional<ro_metavar_env> const & menv);
+inline expr apply_local_context(expr const & a, local_context const & lctx, ro_metavar_env const & menv) { return apply_local_context(a, lctx, some_ro_menv(menv)); }
+inline expr apply_local_context(expr const & a, local_context const & lctx) { return apply_local_context(a, lctx, none_ro_menv()); }
 
 /**
     \brief Extend the local context \c lctx with the entry <tt>lift:s:n</tt>
@@ -305,9 +316,9 @@ local_context add_lift(local_context const & lctx, unsigned s, unsigned n);
    occur in \c m. If s > the maximum free variable that occurs in \c m, then
    we do not add a lift local entry to the local context.
 */
-expr add_lift(expr const & m, unsigned s, unsigned n, optional<metavar_env> const & menv);
-inline expr add_lift(expr const & m, unsigned s, unsigned n) { return add_lift(m, s, n, none_menv()); }
-inline expr add_lift(expr const & m, unsigned s, unsigned n, metavar_env const & menv) { return add_lift(m, s, n, some_menv(menv)); }
+expr add_lift(expr const & m, unsigned s, unsigned n, optional<ro_metavar_env> const & menv);
+inline expr add_lift(expr const & m, unsigned s, unsigned n) { return add_lift(m, s, n, none_ro_menv()); }
+inline expr add_lift(expr const & m, unsigned s, unsigned n, ro_metavar_env const & menv) { return add_lift(m, s, n, some_ro_menv(menv)); }
 
 /**
    \brief Extend the local context \c lctx with the entry <tt>inst:s v</tt>
@@ -323,9 +334,9 @@ local_context add_inst(local_context const & lctx, unsigned s, expr const & v);
    occur in \c m. If s > the maximum free variable that occurs in \c m, then
    we do not add an inst local entry to the local context.
 */
-expr add_inst(expr const & m, unsigned s, expr const & v, optional<metavar_env> const & menv);
-inline expr add_inst(expr const & m, unsigned s, expr const & v) { return add_inst(m, s, v, none_menv()); }
-inline expr add_inst(expr const & m, unsigned s, expr const & v, metavar_env const & menv) { return add_inst(m, s, v, some_menv(menv)); }
+expr add_inst(expr const & m, unsigned s, expr const & v, optional<ro_metavar_env> const & menv);
+inline expr add_inst(expr const & m, unsigned s, expr const & v) { return add_inst(m, s, v, none_ro_menv()); }
+inline expr add_inst(expr const & m, unsigned s, expr const & v, ro_metavar_env const & menv) { return add_inst(m, s, v, some_ro_menv(menv)); }
 
 /**
    \brief Return true iff the given metavariable has a non-empty
@@ -346,7 +357,7 @@ expr pop_meta_context(expr const & m);
 /**
    \brief Return true iff \c e has a metavariable that is assigned in \c menv.
 */
-bool has_assigned_metavar(expr const & e, metavar_env const & menv);
+bool has_assigned_metavar(expr const & e, ro_metavar_env const & menv);
 
 /**
    \brief Return true iff \c e contains the metavariable \c m.
@@ -354,5 +365,5 @@ bool has_assigned_metavar(expr const & e, metavar_env const & menv);
 
    \brief is_metavar(m)
 */
-bool has_metavar(expr const & e, expr const & m, metavar_env const & menv);
+bool has_metavar(expr const & e, expr const & m, ro_metavar_env const & menv);
 }
diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp
index 0039bafb0..4b3d6f2bb 100644
--- a/src/kernel/normalizer.cpp
+++ b/src/kernel/normalizer.cpp
@@ -87,11 +87,11 @@ class normalizer::imp {
     ro_environment env() const { return ro_environment(m_env); }
 
     expr instantiate(expr const & e, unsigned n, expr const * s) {
-        return ::lean::instantiate(e, n, s, m_menv.to_some_menv());
+        return ::lean::instantiate(e, n, s, m_menv.to_some_ro_menv());
     }
 
     expr add_lift(expr const & m, unsigned s, unsigned n) {
-        return ::lean::add_lift(m, s, n, m_menv.to_some_menv());
+        return ::lean::add_lift(m, s, n, m_menv.to_some_ro_menv());
     }
 
     expr lookup(value_stack const & s, unsigned i) {
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index e485f8841..9276e1846 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -43,11 +43,11 @@ class type_checker::imp {
     bool                      m_infer_only;
 
     ro_environment env() const { return ro_environment(m_env); }
-    expr lift_free_vars(expr const & e, unsigned s, unsigned d) { return ::lean::lift_free_vars(e, s, d, m_menv.to_some_menv()); }
-    expr lift_free_vars(expr const & e, unsigned d) { return ::lean::lift_free_vars(e, d, m_menv.to_some_menv()); }
-    expr lower_free_vars(expr const & e, unsigned s, unsigned n) { return ::lean::lower_free_vars(e, s, n, m_menv.to_some_menv()); }
-    expr instantiate_with_closed(expr const & e, expr const & v) { return ::lean::instantiate_with_closed(e, v, m_menv.to_some_menv()); }
-    expr instantiate(expr const & e, expr const & v) { return ::lean::instantiate(e, v, m_menv.to_some_menv()); }
+    expr lift_free_vars(expr const & e, unsigned s, unsigned d) { return ::lean::lift_free_vars(e, s, d, m_menv.to_some_ro_menv()); }
+    expr lift_free_vars(expr const & e, unsigned d) { return ::lean::lift_free_vars(e, d, m_menv.to_some_ro_menv()); }
+    expr lower_free_vars(expr const & e, unsigned s, unsigned n) { return ::lean::lower_free_vars(e, s, n, m_menv.to_some_ro_menv()); }
+    expr instantiate_with_closed(expr const & e, expr const & v) { return ::lean::instantiate_with_closed(e, v, m_menv.to_some_ro_menv()); }
+    expr instantiate(expr const & e, expr const & v) { return ::lean::instantiate(e, v, m_menv.to_some_ro_menv()); }
     expr normalize(expr const & e, context const & ctx, bool unfold_opaque) { return m_normalizer(e, ctx, m_menv.to_some_menv(), unfold_opaque); }
 
     expr check_type(expr const & e, expr const & s, context const & ctx) {
diff --git a/src/library/substitution.cpp b/src/library/substitution.cpp
index 63c01ac4d..b305c8e2b 100644
--- a/src/library/substitution.cpp
+++ b/src/library/substitution.cpp
@@ -23,7 +23,7 @@ expr find(substitution & s, expr e) {
     }
 }
 
-expr apply(substitution & s, expr const & e, optional<metavar_env> const & menv) {
+expr apply(substitution & s, expr const & e, optional<ro_metavar_env> const & menv) {
     return replace(e, [&](expr const & e, unsigned) -> expr {
             if (is_metavar(e)) {
                 expr r = find(s, e);
diff --git a/src/library/substitution.h b/src/library/substitution.h
index 04261619e..931db1e10 100644
--- a/src/library/substitution.h
+++ b/src/library/substitution.h
@@ -20,8 +20,8 @@ typedef splay_map<name, expr, name_quick_cmp> substitution;
 /**
    \brief Apply substitution \c s to \c e
 */
-expr apply(substitution & s, expr const & e, optional<metavar_env> const & menv = none_menv());
-inline expr apply(substitution & s, expr const & e, metavar_env const & menv) { return apply(s, e, some_menv(menv)); }
+expr apply(substitution & s, expr const & e, optional<ro_metavar_env> const & menv = none_ro_menv());
+inline expr apply(substitution & s, expr const & e, ro_metavar_env const & menv) { return apply(s, e, some_ro_menv(menv)); }
 
 expr find(substitution & s, expr e);
 UDATA_DEFS_CORE(substitution)