diff --git a/doc/lean/declarations.org b/doc/lean/declarations.org
index 215f2d0d6..78078962d 100644
--- a/doc/lean/declarations.org
+++ b/doc/lean/declarations.org
@@ -41,69 +41,6 @@ previous example would produce a typing error because the type checker
 would be unable to unfold =id= and establish that =nat= and =id nat=
 are definitionally equal.
 
-** Opaque definitions
-
-Opaque definitions are similar to regular definitions, but they are
-only _transparent_ in the module/file where they were defined.  The
-idea is to allow us to prove theorems about the opaque definition =C=
-in the module where it was defined. In other modules, we can only rely
-on these theorems. That is, the actual definition is
-hidden/encapsulated, and the module designer is free to change it
-without affecting its "customers".
-
-Actually, the opaque definition is only treated as transparent inside of
-other opaque definitions/theorems in the same module.
-
-Here is an example
-
-#+BEGIN_SRC lean
-    import data.nat
-    opaque definition id {A : Type} (a : A) : A := a
-    -- The following command is type correct since it is being executed in the
-    -- same file where id was defined
-    check λ (x : nat) (y : id nat), x = y
-
-    -- The following theorem is also type correct since id is being treated as
-    -- transparent only in the proof by reflexivity.
-    theorem id_eq {A : Type} (a : A) : id a = a :=
-    eq.refl a
-
-    -- The following transparent definition is also type correct. It uses
-    -- id but it can be type checked without unfolding id.
-    definition id2 {A : Type} (a : A) : A :=
-    id a
-
-    -- The following definition is type incorrect. It only type checks if
-    -- we unfold id, but it is not allowed because the definition is opaque.
-    /-
-    definition buggy_def {A : Type} (a : A) : Prop :=
-    ∀ (b : id A), a = b
-    -/
-#+END_SRC
-
-Theorems are always opaque, but we should be able to type check their type
-in any module. The following theorem is type incorrect because we need to
-unfold the opaque definition =id= to type check it.
-
-#+BEGIN_SRC lean
-    import data.unit
-    opaque definition id {A : Type} (a : A) : A := a
-    /-
-    theorem buggy_thm (a : unit) (b : id unit) : a = b :=
-    unit.equal a b
-    -/
-#+END_SRC
-
-In contrast, the following theorem is type correct because =id= is
-transparent in this example.
-
-#+BEGIN_SRC lean
-  import data.unit
-  definition id {A : Type} (a : A) : A := a
-  theorem simple (a : unit) (b : id unit) : a = b :=
-  unit.equal a b
-#+END_SRC
-
 ** Private definitions and theorems
 
 Sometimes it is useful to hide auxiliary definitions and theorems from
diff --git a/library/logic/axioms/hilbert.lean b/library/logic/axioms/hilbert.lean
index e844e3f18..893fa62f5 100644
--- a/library/logic/axioms/hilbert.lean
+++ b/library/logic/axioms/hilbert.lean
@@ -30,7 +30,7 @@ inhabited_of_nonempty (obtain w Hw, from H, nonempty.intro w)
 
 /- the Hilbert epsilon function -/
 
-opaque definition epsilon {A : Type} [H : nonempty A] (P : A → Prop) : A :=
+definition epsilon {A : Type} [H : nonempty A] (P : A → Prop) : A :=
 let u : {x | (∃y, P y) → P x} :=
   strong_indefinite_description P H in
 elt_of u
@@ -39,7 +39,8 @@ theorem epsilon_spec_aux {A : Type} (H : nonempty A) (P : A → Prop) (Hex : ∃
     P (@epsilon A H P) :=
 let u : {x | (∃y, P y) → P x} :=
   strong_indefinite_description P H in
-has_property u Hex
+have aux : (∃y, P y) → P (elt_of (strong_indefinite_description P H)), from has_property u,
+aux Hex
 
 theorem epsilon_spec {A : Type} {P : A → Prop} (Hex : ∃y, P y) :
     P (@epsilon A (nonempty_of_exists Hex) P) :=
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index fd7ab27f9..52d8938f3 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -460,7 +460,7 @@ environment end_scoped_cmd(parser & p) {
 environment check_cmd(parser & p) {
     expr e; level_param_names ls;
     std::tie(e, ls) = parse_local_expr(p);
-    auto tc = mk_type_checker(p.env(), p.mk_ngen(), true);
+    auto tc = mk_type_checker(p.env(), p.mk_ngen());
     expr type = tc->check(e, ls).first;
     auto reg              = p.regular_stream();
     formatter fmt         = reg.get_formatter();
@@ -481,7 +481,7 @@ environment check_cmd(parser & p) {
 class all_transparent_converter : public default_converter {
 public:
     all_transparent_converter(environment const & env):
-        default_converter(env, optional<module_idx>(), true) {
+        default_converter(env) {
     }
     virtual bool is_opaque(declaration const &) const {
         return false;
@@ -502,7 +502,7 @@ environment eval_cmd(parser & p) {
     std::tie(e, ls) = parse_local_expr(p);
     expr r;
     if (whnf) {
-        auto tc = mk_type_checker(p.env(), p.mk_ngen(), true);
+        auto tc = mk_type_checker(p.env(), p.mk_ngen());
         r = tc->whnf(e).first;
     } else if (all_transparent) {
         type_checker tc(p.env(), name_generator(),
@@ -767,7 +767,7 @@ environment telescope_eq_cmd(parser & p) {
         t.push_back(local);
         e = instantiate(binding_body(e), local);
     }
-    auto tc = mk_type_checker(p.env(), p.mk_ngen(), true);
+    auto tc = mk_type_checker(p.env(), p.mk_ngen());
     buffer<expr> eqs;
     mk_telescopic_eq(*tc, t, eqs);
     for (expr const & eq : eqs) {
diff --git a/src/frontends/lean/calc_proof_elaborator.cpp b/src/frontends/lean/calc_proof_elaborator.cpp
index 4b3ce1b1f..d6cb8bde7 100644
--- a/src/frontends/lean/calc_proof_elaborator.cpp
+++ b/src/frontends/lean/calc_proof_elaborator.cpp
@@ -120,7 +120,7 @@ static optional<pair<expr, expr>> apply_subst(environment const & env, local_con
 constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
                                local_context const & _ctx, expr const & m, expr const & _e,
                                constraint_seq const & cs, unifier_config const & cfg,
-                               info_manager * im, bool relax, update_type_info_fn const & fn) {
+                               info_manager * im, update_type_info_fn const & fn) {
     justification j         = mk_failed_to_synthesize_jst(env, m);
     auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & _s,
                          name_generator const & _ngen) {
@@ -128,7 +128,7 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
         expr e            = _e;
         substitution s    = _s;
         name_generator ngen(_ngen);
-        type_checker_ptr tc(mk_type_checker(env, ngen.mk_child(), relax));
+        type_checker_ptr tc(mk_type_checker(env, ngen.mk_child()));
         constraint_seq new_cs = cs;
         expr e_type = tc->infer(e, new_cs);
         e_type      = s.instantiate(e_type);
@@ -163,8 +163,8 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
             fcs.linearize(cs_buffer);
             metavar_closure cls(meta);
             cls.add(meta_type);
-            cls.mk_constraints(s, j, relax, cs_buffer);
-            cs_buffer.push_back(mk_eq_cnstr(meta, e, j, relax));
+            cls.mk_constraints(s, j, cs_buffer);
+            cs_buffer.push_back(mk_eq_cnstr(meta, e, j));
 
             unifier_config new_cfg(cfg);
             new_cfg.m_discard      = false;
@@ -182,7 +182,7 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
                 throw_elaborator_exception("solution contains metavariables", e);
             if (im)
                 im->instantiate(new_s);
-            constraints r = cls.mk_constraints(new_s, j, relax);
+            constraints r = cls.mk_constraints(new_s, j);
             return append(r, postponed);
         };
 
@@ -250,6 +250,6 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
         }
     };
     bool owner = false;
-    return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Epilogue), owner, j, relax);
+    return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Epilogue), owner, j);
 }
 }
diff --git a/src/frontends/lean/calc_proof_elaborator.h b/src/frontends/lean/calc_proof_elaborator.h
index cc3a5dfb8..40ac3153b 100644
--- a/src/frontends/lean/calc_proof_elaborator.h
+++ b/src/frontends/lean/calc_proof_elaborator.h
@@ -23,7 +23,7 @@ typedef std::function<void(expr const &)> update_type_info_fn;
 constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
                                local_context const & ctx, expr const & m, expr const & e,
                                constraint_seq const & cs, unifier_config const & cfg,
-                               info_manager * im, bool relax, update_type_info_fn const & fn);
+                               info_manager * im, update_type_info_fn const & fn);
 
 void initialize_calc_proof_elaborator();
 void finalize_calc_proof_elaborator();
diff --git a/src/frontends/lean/coercion_elaborator.cpp b/src/frontends/lean/coercion_elaborator.cpp
index 2810e0fae..bdb5ebb36 100644
--- a/src/frontends/lean/coercion_elaborator.cpp
+++ b/src/frontends/lean/coercion_elaborator.cpp
@@ -58,7 +58,7 @@ optional<constraints> coercion_elaborator::next() {
     that considers coercions from a_type to the type assigned to \c m. */
 constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
                              expr const & m, expr const & a, expr const & a_type,
-                             justification const & j, unsigned delay_factor, bool relax) {
+                             justification const & j, unsigned delay_factor) {
     auto choice_fn = [=, &tc, &infom](expr const & meta, expr const & d_type, substitution const & s,
                                       name_generator const & /* ngen */) {
         expr          new_a_type;
@@ -74,10 +74,10 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
             if (delay_factor < to_delay_factor(cnstr_group::DelayedChoice)) {
                 // postpone...
                 return lazy_list<constraints>(constraints(mk_coercion_cnstr(tc, infom, m, a, a_type, justification(),
-                                                                            delay_factor+1, relax)));
+                                                                            delay_factor+1)));
             } else {
                 // giveup...
-                return lazy_list<constraints>(constraints(mk_eq_cnstr(meta, a, justification(), relax)));
+                return lazy_list<constraints>(constraints(mk_eq_cnstr(meta, a, justification())));
             }
         }
         constraint_seq cs;
@@ -89,7 +89,7 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
             buffer<constraints> choices;
             buffer<expr> coes;
             // first alternative: no coercion
-            constraint_seq cs1 = cs + mk_eq_cnstr(meta, a, justification(), relax);
+            constraint_seq cs1 = cs + mk_eq_cnstr(meta, a, justification());
             choices.push_back(cs1.to_list());
             unsigned i = alts.size();
             while (i > 0) {
@@ -98,7 +98,7 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
                 expr coe   = std::get<1>(t);
                 expr new_a = copy_tag(a, mk_app(coe, a));
                 coes.push_back(coe);
-                constraint_seq csi = cs + mk_eq_cnstr(meta, new_a, new_a_type_jst, relax);
+                constraint_seq csi = cs + mk_eq_cnstr(meta, new_a, new_a_type_jst);
                 choices.push_back(csi.to_list());
             }
             return choose(std::make_shared<coercion_elaborator>(infom, meta,
@@ -109,23 +109,23 @@ constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
             if (is_nil(coes)) {
                 expr new_a = a;
                 infom.erase_coercion_info(a);
-                cs += mk_eq_cnstr(meta, new_a, new_a_type_jst, relax);
+                cs += mk_eq_cnstr(meta, new_a, new_a_type_jst);
                 return lazy_list<constraints>(cs.to_list());
             } else if (is_nil(tail(coes))) {
                 expr new_a = copy_tag(a, mk_app(head(coes), a));
                 infom.save_coercion_info(a, new_a);
-                cs += mk_eq_cnstr(meta, new_a, new_a_type_jst, relax);
+                cs += mk_eq_cnstr(meta, new_a, new_a_type_jst);
                 return lazy_list<constraints>(cs.to_list());
             } else {
                 list<constraints> choices = map2<constraints>(coes, [&](expr const & coe) {
                         expr new_a   = copy_tag(a, mk_app(coe, a));
-                        constraint c = mk_eq_cnstr(meta, new_a, new_a_type_jst, relax);
+                        constraint c = mk_eq_cnstr(meta, new_a, new_a_type_jst);
                         return (cs + c).to_list();
                     });
                 return choose(std::make_shared<coercion_elaborator>(infom, meta, choices, coes, false));
             }
         }
     };
-    return mk_choice_cnstr(m, choice_fn, delay_factor, true, j, relax);
+    return mk_choice_cnstr(m, choice_fn, delay_factor, true, j);
 }
 }
diff --git a/src/frontends/lean/coercion_elaborator.h b/src/frontends/lean/coercion_elaborator.h
index a3f0d0486..956a0a0ea 100644
--- a/src/frontends/lean/coercion_elaborator.h
+++ b/src/frontends/lean/coercion_elaborator.h
@@ -38,14 +38,11 @@ public:
     enumerate coercion functions \c f. By "not known", we mean the type is a
     metavariable application.
 
-    \param relax True if opaque constants in the current module should be treated
-                 as transparent
-
     \see coercion_info_manager
 */
 constraint mk_coercion_cnstr(type_checker & tc, coercion_info_manager & infom,
                              expr const & m, expr const & a, expr const & a_type,
-                             justification const & j, unsigned delay_factor, bool relax);
+                             justification const & j, unsigned delay_factor);
 
 list<expr> get_coercions_from_to(type_checker & tc, expr const & from_type, expr const & to_type, constraint_seq & cs);
 }
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 55a6abdd5..72aa27eef 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -1143,15 +1143,15 @@ class definition_cmd_fn {
         }
     }
 
-    std::tuple<expr, expr, level_param_names> elaborate_definition(expr const & type, expr const & value, bool is_opaque) {
+    std::tuple<expr, expr, level_param_names> elaborate_definition(expr const & type, expr const & value) {
         if (m_p.profiling()) {
             std::ostringstream msg;
             display_pos(msg);
             msg << " elaboration time for " << m_name;
             timeit timer(m_p.diagnostic_stream().get_stream(), msg.str().c_str());
-            return m_p.elaborate_definition(m_name, type, value, is_opaque);
+            return m_p.elaborate_definition(m_name, type, value);
         } else {
-            return m_p.elaborate_definition(m_name, type, value, is_opaque);
+            return m_p.elaborate_definition(m_name, type, value);
         }
     }
 
@@ -1161,7 +1161,7 @@ class definition_cmd_fn {
     void elaborate_multi() {
         lean_assert(!m_aux_decls.empty());
         level_param_names new_ls;
-        std::tie(m_type, m_value, new_ls) = elaborate_definition(m_type, m_value, m_is_opaque);
+        std::tie(m_type, m_value, new_ls) = elaborate_definition(m_type, m_value);
         new_ls = append(m_ls, new_ls);
         lean_assert(m_aux_types.empty());
         buffer<expr> aux_values;
@@ -1212,7 +1212,7 @@ class definition_cmd_fn {
                     m_p.add_delayed_theorem(m_env, m_real_name, m_ls, type_as_is, m_value);
                     m_env = module::add(m_env, check(mk_axiom(m_real_name, m_ls, m_type)));
                 } else {
-                    std::tie(m_type, m_value, new_ls) = elaborate_definition(type_as_is, m_value, m_is_opaque);
+                    std::tie(m_type, m_value, new_ls) = elaborate_definition(type_as_is, m_value);
                     m_type  = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, m_type));
                     m_value = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, m_value));
                     new_ls = append(m_ls, new_ls);
@@ -1228,7 +1228,7 @@ class definition_cmd_fn {
                     }
                 }
             } else {
-                std::tie(m_type, m_value, new_ls) = elaborate_definition(m_type, m_value, m_is_opaque);
+                std::tie(m_type, m_value, new_ls) = elaborate_definition(m_type, m_value);
                 new_ls = append(m_ls, new_ls);
                 m_type  = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, m_type));
                 m_value = expand_abbreviations(m_env, unfold_untrusted_macros(m_env, m_value));
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 5fe75ec88..0e44bec93 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -68,11 +68,10 @@ struct elaborator::choice_expr_elaborator : public choice_iterator {
     expr          m_type;
     expr          m_choice;
     unsigned      m_idx;
-    bool          m_relax_main_opaque;
     choice_expr_elaborator(elaborator & elab, local_context const & ctx, local_context const & full_ctx,
-                           expr const & meta, expr const & type, expr const & c, bool relax):
+                           expr const & meta, expr const & type, expr const & c):
         m_elab(elab), m_context(ctx), m_full_context(full_ctx), m_meta(meta),
-        m_type(type), m_choice(c), m_idx(get_num_choices(m_choice)), m_relax_main_opaque(relax) {
+        m_type(type), m_choice(c), m_idx(get_num_choices(m_choice)) {
     }
 
     virtual optional<constraints> next() {
@@ -93,13 +92,12 @@ struct elaborator::choice_expr_elaborator : public choice_iterator {
                     expr r_type                = m_elab.infer_type(r, new_cs);
                     if (!has_expr_metavar_relaxed(r_type)) {
                         cs = new_cs;
-                        auto new_rcs                   = m_elab.ensure_has_type(r, r_type, m_type, justification(),
-                                                                                m_relax_main_opaque);
+                        auto new_rcs                   = m_elab.ensure_has_type(r, r_type, m_type, justification());
                         r                              = new_rcs.first;
                         cs                            += new_rcs.second;
                     }
                 }
-                cs = mk_eq_cnstr(m_meta, r, justification(), m_relax_main_opaque) + cs;
+                cs = mk_eq_cnstr(m_meta, r, justification()) + cs;
                 return optional<constraints>(cs.to_list());
             } catch (exception &) {}
         }
@@ -114,12 +112,10 @@ elaborator::elaborator(elaborator_context & ctx, name_generator const & ngen, bo
     m_full_context(),
     m_unifier_config(ctx.m_ios.get_options(), true /* use exceptions */, true /* discard */) {
     m_has_sorry = has_sorry(m_ctx.m_env);
-    m_relax_main_opaque = false;
     m_use_tactic_hints  = true;
     m_no_info           = false;
     m_in_equation_lhs   = false;
-    m_tc[0]             = mk_type_checker(ctx.m_env, m_ngen.mk_child(), false);
-    m_tc[1]             = mk_type_checker(ctx.m_env, m_ngen.mk_child(), true);
+    m_tc                = mk_type_checker(ctx.m_env, m_ngen.mk_child());
     m_nice_mvar_names   = nice_mvar_names;
 }
 
@@ -131,8 +127,6 @@ void elaborator::register_meta(expr const & meta) {
     lean_assert(is_meta(meta));
     name const & n = mlocal_name(get_app_fn(meta));
     m_mvar2meta.insert(n, meta);
-    if (m_relax_main_opaque)
-        m_relaxed_mvars.insert(n);
 }
 
 /** \brief Convert the metavariable to the metavariable application that captures
@@ -153,7 +147,7 @@ void elaborator::save_type_data(expr const & e, expr const & r) {
         (is_constant(e) || is_local(e) || is_placeholder(e) || is_as_atomic(e) ||
          is_consume_args(e) || is_notation_info(e))) {
         if (auto p = pip()->get_pos_info(e)) {
-            expr t = m_tc[m_relax_main_opaque]->infer(r).first;
+            expr t = m_tc->infer(r).first;
             m_pre_info_data.add_type_info(p->first, p->second, t);
         }
     }
@@ -172,7 +166,7 @@ void elaborator::save_binder_type(expr const & e, expr const & r) {
 void elaborator::save_extra_type_data(expr const & e, expr const & r) {
     if (!m_no_info && infom() && pip()) {
         if (auto p = pip()->get_pos_info(e)) {
-            expr t = m_tc[m_relax_main_opaque]->infer(r).first;
+            expr t = m_tc->infer(r).first;
             m_pre_info_data.add_extra_type_info(p->first, p->second, r, t);
         }
     }
@@ -216,7 +210,7 @@ void elaborator::save_placeholder_info(expr const & e, expr const & r) {
 void elaborator::save_coercion_info(expr const & e, expr const & c) {
     if (!m_no_info && infom() && pip()) {
         if (auto p = pip()->get_pos_info(e)) {
-            expr t = m_tc[m_relax_main_opaque]->infer(c).first;
+            expr t = m_tc->infer(c).first;
             m_pre_info_data.add_coercion_info(p->first, p->second, c, t);
         }
     }
@@ -253,7 +247,7 @@ expr elaborator::mk_placeholder_meta(optional<name> const & suffix, optional<exp
                                      tag g, bool is_strict, bool is_inst_implicit, constraint_seq & cs) {
     if (is_inst_implicit && !m_ctx.m_ignore_instances) {
         auto ec = mk_class_instance_elaborator(
-            env(), ios(), m_context, m_ngen.next(), suffix, m_relax_main_opaque,
+            env(), ios(), m_context, m_ngen.next(), suffix,
             use_local_instances(), is_strict, type, g, m_unifier_config, m_ctx.m_pos_provider);
         register_meta(ec.first);
         cs += ec.second;
@@ -299,15 +293,14 @@ expr elaborator::visit_choice(expr const & e, optional<expr> const & t, constrai
     // Possible optimization: try to lookahead and discard some of the alternatives.
     expr m                 = m_full_context.mk_meta(m_ngen, t, e.get_tag());
     register_meta(m);
-    bool relax             = m_relax_main_opaque;
     local_context ctx      = m_context;
     local_context full_ctx = m_full_context;
     auto fn = [=](expr const & meta, expr const & type, substitution const & /* s */,
                   name_generator const & /* ngen */) {
-        return choose(std::make_shared<choice_expr_elaborator>(*this, ctx, full_ctx, meta, type, e, relax));
+        return choose(std::make_shared<choice_expr_elaborator>(*this, ctx, full_ctx, meta, type, e));
     };
     justification j = mk_justification("none of the overloads is applicable", some_expr(e));
-    cs += mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), true, j, m_relax_main_opaque);
+    cs += mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), true, j);
     return m;
 }
 
@@ -340,7 +333,7 @@ expr elaborator::visit_calc_proof(expr const & e, optional<expr> const & t, cons
     auto fn = [=](expr const & t) { save_type_data(get_annotation_arg(e), t); };
     constraint c                   = mk_calc_proof_cnstr(env(), ios().get_options(),
                                                          m_context, m, ecs.first, ecs.second, m_unifier_config,
-                                                         im, m_relax_main_opaque, fn);
+                                                         im, fn);
     cs += c;
     return m;
 }
@@ -353,8 +346,8 @@ static bool is_implicit_pi(expr const & e) {
 }
 
 /** \brief Auxiliary function for adding implicit arguments to coercions to function-class */
-expr elaborator::add_implict_args(expr e, constraint_seq & cs, bool relax) {
-    type_checker & tc = *m_tc[relax];
+expr elaborator::add_implict_args(expr e, constraint_seq & cs) {
+    type_checker & tc = *m_tc;
     constraint_seq new_cs;
     expr type = tc.whnf(tc.infer(e, new_cs), new_cs);
     if (!is_implicit_pi(type))
@@ -395,10 +388,10 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
     if (!is_pi(f_type) && has_metavar(f_type)) {
         constraint_seq saved_cs = cs;
         expr new_f_type = whnf(f_type, cs);
-        if (!is_pi(new_f_type) && m_tc[m_relax_main_opaque]->is_stuck(new_f_type)) {
+        if (!is_pi(new_f_type) && m_tc->is_stuck(new_f_type)) {
             cs = saved_cs;
             // let type checker add constraint
-            f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f, cs);
+            f_type = m_tc->ensure_pi(f_type, f, cs);
         } else {
             f_type = new_f_type;
         }
@@ -410,14 +403,12 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
             throw_kernel_exception(env(), f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); });
         } else if (is_nil(tail(coes))) {
             expr old_f = f;
-            bool relax = m_relax_main_opaque;
             f = mk_coercion_app(head(coes), f);
-            f = add_implict_args(f, cs, relax);
+            f = add_implict_args(f, cs);
             f_type = infer_type(f, cs);
             save_coercion_info(old_f, f);
             lean_assert(is_pi(f_type));
         } else {
-            bool relax             = m_relax_main_opaque;
             local_context ctx      = m_context;
             local_context full_ctx = m_full_context;
             justification j        = mk_justification(f, [=](formatter const & fmt, substitution const & subst) {
@@ -429,19 +420,19 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
                 list<constraints> choices = map2<constraints>(coes, [&](expr const & coe) {
                         expr new_f      = mk_coercion_app(coe, f);
                         constraint_seq cs;
-                        new_f = add_implict_args(new_f, cs, relax);
-                        cs += mk_eq_cnstr(meta, new_f, j, relax);
+                        new_f = add_implict_args(new_f, cs);
+                        cs += mk_eq_cnstr(meta, new_f, j);
                         return cs.to_list();
                     });
                 return choose(std::make_shared<coercion_elaborator>(*this, f, choices, coes, false));
             };
             f   = m_full_context.mk_meta(m_ngen, none_expr(), f.get_tag());
             register_meta(f);
-            cs += mk_choice_cnstr(f, choice_fn, to_delay_factor(cnstr_group::Basic), true, j, relax);
+            cs += mk_choice_cnstr(f, choice_fn, to_delay_factor(cnstr_group::Basic), true, j);
             lean_assert(is_meta(f));
             // let type checker add constraint
             f_type = infer_type(f, cs);
-            f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f, cs);
+            f_type = m_tc->ensure_pi(f_type, f, cs);
             lean_assert(is_pi(f_type));
         }
     } else {
@@ -481,7 +472,7 @@ expr elaborator::apply_coercion(expr const & a, expr a_type, expr d_type) {
     a_type = whnf(a_type).first;
     d_type = whnf(d_type).first;
     constraint_seq aux_cs;
-    list<expr> coes = get_coercions_from_to(*m_tc[m_relax_main_opaque], a_type, d_type, aux_cs);
+    list<expr> coes = get_coercions_from_to(*m_tc, a_type, d_type, aux_cs);
     if (is_nil(coes)) {
         erase_coercion_info(a);
         return a;
@@ -494,7 +485,7 @@ expr elaborator::apply_coercion(expr const & a, expr a_type, expr d_type) {
             expr r = mk_coercion_app(coe, a);
             expr r_type = infer_type(r).first;
             try {
-                if (m_tc[m_relax_main_opaque]->is_def_eq(r_type, d_type).first) {
+                if (m_tc->is_def_eq(r_type, d_type).first) {
                     save_coercion_info(a, r);
                     return r;
                 }
@@ -510,21 +501,17 @@ expr elaborator::apply_coercion(expr const & a, expr a_type, expr d_type) {
 pair<expr, constraint_seq> elaborator::mk_delayed_coercion(
     expr const & a, expr const & a_type, expr const & expected_type,
     justification const & j) {
-    bool relax = m_relax_main_opaque;
-    type_checker & tc = *m_tc[relax];
+    type_checker & tc = *m_tc;
     expr m       = m_full_context.mk_meta(m_ngen, some_expr(expected_type), a.get_tag());
     register_meta(m);
-    constraint c = mk_coercion_cnstr(tc, *this, m, a, a_type, j, to_delay_factor(cnstr_group::Basic), relax);
+    constraint c = mk_coercion_cnstr(tc, *this, m, a, a_type, j, to_delay_factor(cnstr_group::Basic));
     return to_ecs(m, c);
 }
 
 /** \brief Given a term <tt>a : a_type</tt>, ensure it has type \c expected_type. Apply coercions if needed
-
-    \remark relax == true affects how opaque definitions in the main module are treated.
 */
 pair<expr, constraint_seq> elaborator::ensure_has_type(
-    expr const & a, expr const & a_type, expr const & expected_type,
-    justification const & j, bool relax) {
+        expr const & a, expr const & a_type, expr const & expected_type, justification const & j) {
     if (is_meta(expected_type) && has_coercions_from(a_type)) {
         return mk_delayed_coercion(a, a_type, expected_type, j);
     } else if (!m_in_equation_lhs && is_meta(a_type) && has_coercions_to(expected_type)) {
@@ -532,7 +519,7 @@ pair<expr, constraint_seq> elaborator::ensure_has_type(
     } else {
         pair<bool, constraint_seq> dcs;
         try {
-            dcs = m_tc[relax]->is_def_eq(a_type, expected_type, j);
+            dcs = m_tc->is_def_eq(a_type, expected_type, j);
         } catch (exception&) {
             dcs.first = false;
         }
@@ -545,7 +532,7 @@ pair<expr, constraint_seq> elaborator::ensure_has_type(
             if (!is_eqp(a, new_a)) {
                 expr new_a_type = infer_type(new_a, cs);
                 try {
-                    coercion_worked = m_tc[relax]->is_def_eq(new_a_type, expected_type, j, cs);
+                    coercion_worked = m_tc->is_def_eq(new_a_type, expected_type, j, cs);
                 } catch (exception&) {
                     coercion_worked = false;
                 }
@@ -554,7 +541,7 @@ pair<expr, constraint_seq> elaborator::ensure_has_type(
                 return to_ecs(new_a, cs);
             } else if (has_metavar(a_type) || has_metavar(expected_type)) {
                 // rely on unification hints to solve this constraint
-                return to_ecs(a, mk_eq_cnstr(a_type, expected_type, j, relax));
+                return to_ecs(a, mk_eq_cnstr(a_type, expected_type, j));
             } else {
                 throw unifier_exception(j, substitution());
             }
@@ -636,7 +623,7 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) {
         expr a_type     = infer_type(a, a_cs);
         expr r          = mk_app(f, a, e.get_tag());
         justification j = mk_app_justification(r, a, d_type, a_type);
-        auto new_a_cs   = ensure_has_type(a, a_type, d_type, j, m_relax_main_opaque);
+        auto new_a_cs   = ensure_has_type(a, a_type, d_type, j);
         expr new_a      = new_a_cs.first;
         cs += f_cs + new_a_cs.second + a_cs;
         return update_app(r, app_fn(r), new_a);
@@ -722,7 +709,7 @@ expr elaborator::ensure_type(expr const & e, constraint_seq & cs) {
             return e;
         if (is_meta(t)) {
             // let type checker add constraint
-            m_tc[m_relax_main_opaque]->ensure_sort(t, e, cs);
+            m_tc->ensure_sort(t, e, cs);
             return e;
         }
     }
@@ -811,7 +798,7 @@ expr elaborator::visit_typed_expr(expr const & e, constraint_seq & cs) {
     expr v      = visit(get_typed_expr_expr(e), v_cs);
     expr v_type = infer_type(v, v_cs);
     justification j = mk_type_mismatch_jst(v, v_type, t, e);
-    auto new_vcs    = ensure_has_type(v, v_type, t, j, m_relax_main_opaque);
+    auto new_vcs    = ensure_has_type(v, v_type, t, j);
     v = new_vcs.first;
     cs += t_cs + new_vcs.second + v_cs;
     return v;
@@ -1060,7 +1047,6 @@ static expr assign_equation_lhs_metas(type_checker & tc, expr const & eqns) {
 
 // \remark original_eqns is eqns before elaboration
 constraint elaborator::mk_equations_cnstr(expr const & m, expr const & eqns) {
-    bool relax               = m_relax_main_opaque;
     environment const & _env = env();
     io_state const & _ios    = ios();
     justification j          = mk_failed_to_synthesize_jst(_env, m);
@@ -1071,15 +1057,15 @@ constraint elaborator::mk_equations_cnstr(expr const & m, expr const & eqns) {
         new_eqns            = solve_unassigned_mvars(new_s, new_eqns);
         if (display_unassigned_mvars(new_eqns, new_s))
             return lazy_list<constraints>();
-        type_checker_ptr tc = mk_type_checker(_env, ngen, relax);
+        type_checker_ptr tc = mk_type_checker(_env, ngen);
         new_eqns            = assign_equation_lhs_metas(*tc, new_eqns);
-        expr val            = compile_equations(*tc, _ios, new_eqns, meta, meta_type, relax);
+        expr val            = compile_equations(*tc, _ios, new_eqns, meta, meta_type);
         justification j     = mk_justification("equation compilation", some_expr(eqns));
-        constraint c        = mk_eq_cnstr(meta, val, j, relax);
+        constraint c        = mk_eq_cnstr(meta, val, j);
         return lazy_list<constraints>(c);
     };
     bool owner = true;
-    return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), owner, j, relax);
+    return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), owner, j);
 }
 
 expr elaborator::visit_equations(expr const & eqns, constraint_seq & cs) {
@@ -1100,7 +1086,7 @@ expr elaborator::visit_equations(expr const & eqns, constraint_seq & cs) {
         expr wf         = visit(mk_constant(get_well_founded_name()), cs);
         wf              = ::lean::mk_app(wf, *new_R);
         justification j = mk_type_mismatch_jst(*new_Hwf, Hwf_type, wf, equations_wf_proof(eqns));
-        auto new_Hwf_cs = ensure_has_type(*new_Hwf, Hwf_type, wf, j, m_relax_main_opaque);
+        auto new_Hwf_cs = ensure_has_type(*new_Hwf, Hwf_type, wf, j);
         new_Hwf         = new_Hwf_cs.first;
         cs             += new_Hwf_cs.second;
     }
@@ -1188,7 +1174,7 @@ expr elaborator::visit_equation(expr const & eq, constraint_seq & cs) {
             substitution s(subst);
             return pp_def_type_mismatch(fmt, local_pp_name(lhs_fn), s.instantiate(lhs_type), s.instantiate(rhs_type));
         });
-    pair<expr, constraint_seq> new_rhs_cs = ensure_has_type(new_rhs, rhs_type, lhs_type, j, m_relax_main_opaque);
+    pair<expr, constraint_seq> new_rhs_cs = ensure_has_type(new_rhs, rhs_type, lhs_type, j);
     new_rhs = new_rhs_cs.first;
     cs     += new_rhs_cs.second;
     return copy_tag(eq, mk_equation(new_lhs, new_rhs));
@@ -1216,7 +1202,7 @@ expr elaborator::visit_decreasing(expr const & e, constraint_seq & cs) {
     expr dec_proof      = visit(decreasing_proof(e), cs);
     expr f_type         = mlocal_type(get_app_fn(*m_equation_lhs));
     buffer<expr> ts;
-    type_checker & tc = *m_tc[m_relax_main_opaque];
+    type_checker & tc = *m_tc;
     to_telescope(tc, f_type, ts, optional<binder_info>(), cs);
     buffer<expr> old_args;
     buffer<expr> new_args;
@@ -1229,7 +1215,7 @@ expr elaborator::visit_decreasing(expr const & e, constraint_seq & cs) {
     expr expected_dec_proof_type = mk_app(mk_app(*m_equation_R, new_tuple, e.get_tag()), old_tuple, e.get_tag());
     expr dec_proof_type = infer_type(dec_proof, cs);
     justification j = mk_type_mismatch_jst(dec_proof, dec_proof_type, expected_dec_proof_type, decreasing_proof(e));
-    auto new_dec_proof_cs = ensure_has_type(dec_proof, dec_proof_type, expected_dec_proof_type, j, m_relax_main_opaque);
+    auto new_dec_proof_cs = ensure_has_type(dec_proof, dec_proof_type, expected_dec_proof_type, j);
     dec_proof = new_dec_proof_cs.first;
     cs       += new_dec_proof_cs.second;
     return mk_decreasing(dec_app, dec_proof);
@@ -1334,7 +1320,7 @@ expr elaborator::visit_structure_instance(expr const & e, constraint_seq & cs) {
         S_mk            = mk_app(S_mk, v, result_tag);
         expr v_type     = infer_type(v, cs);
         justification j = mk_app_justification(S_mk, v, d_type, v_type);
-        auto new_v_cs   = ensure_has_type(v, v_type, d_type, j, m_relax_main_opaque);
+        auto new_v_cs   = ensure_has_type(v, v_type, d_type, j);
         expr new_v      = new_v_cs.first;
         cs             += new_v_cs.second;
         S_mk            = update_app(S_mk, app_fn(S_mk), new_v);
@@ -1438,7 +1424,7 @@ expr elaborator::process_obtain_expr(list<obtain_struct> const & s_list, list<ex
         check_R_type();
         expr minor_type = whnf(binding_domain(R_type), cs);
         buffer<expr> telescope;
-        to_telescope(*m_tc[m_relax_main_opaque], minor_type, telescope, optional<binder_info>(), cs);
+        to_telescope(*m_tc, minor_type, telescope, optional<binder_info>(), cs);
         lean_assert(!s.is_leaf());
         buffer<obtain_struct> s_buffer;
         to_buffer(s.get_children(), s_buffer);
@@ -1638,7 +1624,6 @@ optional<expr> elaborator::get_pre_tactic_for(expr const & mvar) {
 
 optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac) {
     try {
-        bool relax = m_relax_main_opaque;
         auto fn = [=](goal const & g, name_generator const & ngen, expr const & e, optional<expr> const & expected_type,
                       substitution const & subst, bool report_unassigned) {
             elaborator aux_elaborator(m_ctx, ngen);
@@ -1646,7 +1631,7 @@ optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac) {
             // We must do it otherwise, it is easy to make the system loop.
             bool use_tactic_hints = false;
             return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e,
-                                                   relax, use_tactic_hints, subst, report_unassigned);
+                                                   use_tactic_hints, subst, report_unassigned);
         };
         return optional<tactic>(expr_to_tactic(env(), fn, pre_tac, pip()));
     } catch (expr_to_tactic_exception & ex) {
@@ -1813,11 +1798,10 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set
         return;
     meta = instantiate_meta(*meta, subst);
     // TODO(Leo): we are discarding constraints here
-    expr type = m_tc[m_relax_main_opaque]->infer(*meta).first;
+    expr type = m_tc->infer(*meta).first;
     // first solve unassigned metavariables in type
     type = solve_unassigned_mvars(subst, type, visited);
-    bool relax_main_opaque = m_relaxed_mvars.contains(mlocal_name(mvar));
-    proof_state ps = to_proof_state(*meta, type, subst, m_ngen.mk_child(), relax_main_opaque);
+    proof_state ps = to_proof_state(*meta, type, subst, m_ngen.mk_child());
     if (auto pre_tac = get_pre_tactic_for(mvar)) {
         if (is_begin_end_annotation(*pre_tac)) {
             try_using_begin_end(subst, mvar, ps, *pre_tac);
@@ -1924,8 +1908,7 @@ bool elaborator::display_unassigned_mvars(expr const & e, substitution const & s
                     expr meta      = tmp_s.instantiate(*it);
                     expr meta_type = tmp_s.instantiate(type_checker(env()).infer(meta).first);
                     goal g(meta, meta_type);
-                    bool relax     = true;
-                    proof_state ps(goals(g), s, m_ngen, constraints(), relax);
+                    proof_state ps(goals(g), s, m_ngen, constraints());
                     display_unsolved_proof_state(mvar, ps, "don't know how to synthesize placeholder");
                     r = true;
                 }
@@ -1982,11 +1965,10 @@ std::tuple<expr, level_param_names> elaborator::apply(substitution & s, expr con
     return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end()));
 }
 
-auto elaborator::operator()(list<expr> const & ctx, expr const & e, bool _ensure_type, bool relax_main_opaque)
+auto elaborator::operator()(list<expr> const & ctx, expr const & e, bool _ensure_type)
 -> std::tuple<expr, level_param_names> {
     m_context.set_ctx(ctx);
     m_full_context.set_ctx(ctx);
-    flet<bool> set_relax(m_relax_main_opaque, relax_main_opaque);
     constraint_seq cs;
     expr r = visit(e, cs);
     if (_ensure_type)
@@ -2000,12 +1982,10 @@ auto elaborator::operator()(list<expr> const & ctx, expr const & e, bool _ensure
     return result;
 }
 
-std::tuple<expr, expr, level_param_names> elaborator::operator()(
-    expr const & t, expr const & v, name const & n, bool is_opaque) {
+std::tuple<expr, expr, level_param_names> elaborator::operator()(expr const & t, expr const & v, name const & n) {
     constraint_seq t_cs;
     expr r_t      = ensure_type(visit(t, t_cs), t_cs);
     // 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);
     constraint_seq v_cs;
     expr r_v      = visit(v, v_cs);
     expr r_v_type = infer_type(r_v, v_cs);
@@ -2013,7 +1993,7 @@ std::tuple<expr, expr, level_param_names> elaborator::operator()(
             substitution s(subst);
             return pp_def_type_mismatch(fmt, n, s.instantiate(r_t), s.instantiate(r_v_type));
         });
-    pair<expr, constraint_seq> r_v_cs = ensure_has_type(r_v, r_v_type, r_t, j, is_opaque);
+    pair<expr, constraint_seq> r_v_cs = ensure_has_type(r_v, r_v_type, r_t, j);
     r_v = r_v_cs.first;
     constraint_seq cs = t_cs + r_v_cs.second + v_cs;
     auto p  = solve(cs).pull();
@@ -2068,7 +2048,7 @@ static expr translate(environment const & env, list<expr> const & ctx, expr cons
 
 /** \brief Elaborate expression \c e in context \c ctx. */
 elaborate_result elaborator::elaborate_nested(list<expr> const & ctx, optional<expr> const & expected_type,
-                                              expr const & n, bool relax, bool use_tactic_hints,
+                                              expr const & n, bool use_tactic_hints,
                                               substitution const & subst, bool report_unassigned) {
     if (infom()) {
         if (auto ps = get_info_tactic_proof_state()) {
@@ -2084,7 +2064,6 @@ elaborate_result elaborator::elaborate_nested(list<expr> const & ctx, optional<e
     m_context.set_ctx(ctx);
     m_context.set_ctx(ctx);
     m_full_context.set_ctx(ctx);
-    flet<bool> set_relax(m_relax_main_opaque, relax);
     flet<bool> set_discard(m_unifier_config.m_discard, false);
     flet<bool> set_use_hints(m_use_tactic_hints, use_tactic_hints);
     constraint_seq cs;
@@ -2104,7 +2083,7 @@ elaborate_result elaborator::elaborate_nested(list<expr> const & ctx, optional<e
         display_unassigned_mvars(r, new_subst);
     if (expected_type) {
         justification j;
-        rcs = append(rcs, cls.mk_constraints(new_subst, j, relax));
+        rcs = append(rcs, cls.mk_constraints(new_subst, j));
     }
     return elaborate_result(r, new_subst, rcs);
 }
@@ -2112,13 +2091,13 @@ elaborate_result elaborator::elaborate_nested(list<expr> const & ctx, optional<e
 static name * g_tmp_prefix = nullptr;
 
 std::tuple<expr, level_param_names> elaborate(elaborator_context & env, list<expr> const & ctx, expr const & e,
-                                              bool relax_main_opaque, bool ensure_type, bool nice_mvar_names) {
-    return elaborator(env, name_generator(*g_tmp_prefix), nice_mvar_names)(ctx, e, ensure_type, relax_main_opaque);
+                                              bool ensure_type, bool nice_mvar_names) {
+    return elaborator(env, name_generator(*g_tmp_prefix), nice_mvar_names)(ctx, e, ensure_type);
 }
 
-std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v,
-                                                    bool is_opaque) {
-    return elaborator(env, name_generator(*g_tmp_prefix))(t, v, n, is_opaque);
+std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t,
+                                                    expr const & v) {
+    return elaborator(env, name_generator(*g_tmp_prefix))(t, v, n);
 }
 
 void initialize_elaborator() {
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 64a27f21b..8d1ddaf93 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -32,14 +32,12 @@ class elaborator : public coercion_info_manager {
     typedef std::vector<pair<expr, expr>> to_check_sorts;
     elaborator_context & m_ctx;
     name_generator       m_ngen;
-    type_checker_ptr     m_tc[2];
+    type_checker_ptr     m_tc;
     // mapping from metavariable ?m to the (?m l_1 ... l_n) where [l_1 ... l_n] are the local constants
     // representing the context where ?m was created.
     local_context        m_context; // current local context: a list of local constants
     local_context        m_full_context; // superset of m_context, it also contains non-contextual locals.
     mvar2meta            m_mvar2meta;
-    // Set of metavariable that where created when m_relax_main_opaque flag is set to true.
-    name_set             m_relaxed_mvars;
     cache                m_cache;
     // The following vector contains sorts that we should check
     // whether the computed universe is too specific or not.
@@ -50,8 +48,6 @@ class elaborator : public coercion_info_manager {
     local_tactic_hints   m_local_tactic_hints;
     // set of metavariables that we already reported unsolved/unassigned
     name_set             m_displayed_errors;
-    // if m_relax_main_opaque is true, then treat opaque definitions from the main module as transparent.
-    bool                 m_relax_main_opaque;
     // if m_no_info is true, we do not collect information when true,
     // we set is to true whenever we find no_info annotation.
     bool                 m_no_info;
@@ -82,12 +78,12 @@ class elaborator : public coercion_info_manager {
 
     expr mk_local(name const & n, expr const & t, binder_info const & bi);
 
-    pair<expr, constraint_seq> infer_type(expr const & e) { return m_tc[m_relax_main_opaque]->infer(e); }
-    pair<expr, constraint_seq> whnf(expr const & e) { return m_tc[m_relax_main_opaque]->whnf(e); }
-    expr infer_type(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->infer(e, s); }
-    expr whnf(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->whnf(e, s); }
+    pair<expr, constraint_seq> infer_type(expr const & e) { return m_tc->infer(e); }
+    pair<expr, constraint_seq> whnf(expr const & e) { return m_tc->whnf(e); }
+    expr infer_type(expr const & e, constraint_seq & s) { return m_tc->infer(e, s); }
+    expr whnf(expr const & e, constraint_seq & s) { return m_tc->whnf(e, s); }
     bool is_def_eq(expr const & e1, expr const & e2, justification const & j, constraint_seq & cs) {
-        return m_tc[m_relax_main_opaque]->is_def_eq(e1, e2, j, cs);
+        return m_tc->is_def_eq(e1, e2, j, cs);
     }
     expr mk_app(expr const & f, expr const & a, tag g) { return ::lean::mk_app(f, a, g); }
 
@@ -118,7 +114,7 @@ class elaborator : public coercion_info_manager {
     expr visit_by(expr const & e, optional<expr> const & t, constraint_seq & cs);
     expr visit_by_plus(expr const & e, optional<expr> const & t, constraint_seq & cs);
     expr visit_calc_proof(expr const & e, optional<expr> const & t, constraint_seq & cs);
-    expr add_implict_args(expr e, constraint_seq & cs, bool relax);
+    expr add_implict_args(expr e, constraint_seq & cs);
     pair<expr, expr> ensure_fun(expr f, constraint_seq & cs);
     bool has_coercions_from(expr const & a_type);
     bool has_coercions_to(expr d_type);
@@ -126,7 +122,7 @@ class elaborator : public coercion_info_manager {
     pair<expr, constraint_seq> mk_delayed_coercion(expr const & a, expr const & a_type, expr const & expected_type,
                                                    justification const & j);
     pair<expr, constraint_seq> ensure_has_type(expr const & a, expr const & a_type, expr const & expected_type,
-                                               justification const & j, bool relax);
+                                               justification const & j);
 
     bool is_choice_app(expr const & e);
     expr visit_choice_app(expr const & e, constraint_seq & cs);
@@ -167,7 +163,7 @@ class elaborator : public coercion_info_manager {
     expr apply(substitution & s, expr const & e, name_set & univ_params, buffer<name> & new_params);
     std::tuple<expr, level_param_names> apply(substitution & s, expr const & e);
     elaborate_result elaborate_nested(list<expr> const & ctx, optional<expr> const & expected_type, expr const & e,
-                                      bool relax, bool use_tactic_hints, substitution const &, bool report_unassigned);
+                                      bool use_tactic_hints, substitution const &, bool report_unassigned);
 
     expr const & get_equation_fn(expr const & eq) const;
     expr visit_equations(expr const & eqns, constraint_seq & cs);
@@ -184,16 +180,14 @@ class elaborator : public coercion_info_manager {
     expr visit_obtain_expr(expr const & e, constraint_seq & cs);
 public:
     elaborator(elaborator_context & ctx, name_generator const & ngen, bool nice_mvar_names = false);
-    std::tuple<expr, level_param_names> operator()(list<expr> const & ctx, expr const & e, bool _ensure_type,
-                                                   bool relax_main_opaque);
-    std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n, bool is_opaque);
+    std::tuple<expr, level_param_names> operator()(list<expr> const & ctx, expr const & e, bool _ensure_type);
+    std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n);
 };
 
 std::tuple<expr, level_param_names> elaborate(elaborator_context & env, list<expr> const & ctx, expr const & e,
-                                              bool relax_main_opaque, bool ensure_type = false, bool nice_mvar_names = false);
+                                              bool ensure_type = false, bool nice_mvar_names = false);
 
-std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v,
-                                                    bool is_opaque);
+std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v);
 void initialize_elaborator();
 void finalize_elaborator();
 }
diff --git a/src/frontends/lean/find_cmd.cpp b/src/frontends/lean/find_cmd.cpp
index 9bea2daf4..a98f8e2d2 100644
--- a/src/frontends/lean/find_cmd.cpp
+++ b/src/frontends/lean/find_cmd.cpp
@@ -73,7 +73,7 @@ bool match_pattern(type_checker & tc, expr const & pattern, declaration const &
         cfg.m_max_steps            = max_steps;
         cfg.m_kind                 = cheap ? unifier_kind::Cheap : unifier_kind::Liberal;
         cfg.m_ignore_context_check = true;
-        auto r = unify(tc.env(), pattern, dt, tc.mk_ngen(), true, substitution(), cfg);
+        auto r = unify(tc.env(), pattern, dt, tc.mk_ngen(), substitution(), cfg);
         return static_cast<bool>(r.pull());
     } catch (exception&) {
         return false;
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index f7f0f9f8c..ade6bb1b6 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -113,7 +113,7 @@ struct inductive_cmd_fn {
         m_u = mk_global_univ(u_name);
         m_infer_result_universe = false;
         m_namespace = get_namespace(m_env);
-        m_tc = mk_type_checker(m_env, m_p.mk_ngen(), false);
+        m_tc = mk_type_checker(m_env, m_p.mk_ngen());
     }
 
     [[ noreturn ]] void throw_error(char const * error_msg) { throw parser_error(error_msg, m_pos); }
diff --git a/src/frontends/lean/migrate_cmd.cpp b/src/frontends/lean/migrate_cmd.cpp
index b45462365..661b1d50f 100644
--- a/src/frontends/lean/migrate_cmd.cpp
+++ b/src/frontends/lean/migrate_cmd.cpp
@@ -45,7 +45,7 @@ class migrate_converter : public unfold_semireducible_converter {
     list<name> m_namespaces;
 public:
     migrate_converter(environment const & env, list<name> const & ns):
-        unfold_semireducible_converter(env, true, true),
+        unfold_semireducible_converter(env, true),
         m_namespaces(ns) {
     }
 
@@ -420,7 +420,7 @@ struct migrate_cmd_fn {
         m_migrate_tc = std::unique_ptr<type_checker>(new type_checker(m_env, m_ngen.mk_child(),
                        std::unique_ptr<converter>(new migrate_converter(m_env, get_namespaces(m_env)))));
         m_tc = std::unique_ptr<type_checker>(new type_checker(m_env, m_ngen.mk_child(),
-               std::unique_ptr<converter>(new unfold_semireducible_converter(m_env, true, true))));
+               std::unique_ptr<converter>(new unfold_semireducible_converter(m_env, true))));
 
         parse_params();
         parse_from_namespace();
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 1bf3079d6..64838b96d 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -720,65 +720,60 @@ elaborator_context parser::mk_elaborator_context(environment const & env, local_
 }
 
 std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, list<expr> const & ctx) {
-    bool relax            = true;
     bool check_unassigned = false;
     bool ensure_type      = false;
     bool nice_mvar_names  = true;
     parser_pos_provider pp = get_pos_provider();
     elaborator_context env = mk_elaborator_context(pp, check_unassigned);
-    auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type, nice_mvar_names);
+    auto r = ::lean::elaborate(env, ctx, e, ensure_type, nice_mvar_names);
     m_pre_info_manager.clear();
     return r;
 }
 
 std::tuple<expr, level_param_names> parser::elaborate(expr const & e, list<expr> const & ctx) {
-    bool relax            = false;
     bool check_unassigned = true;
     bool ensure_type      = false;
     parser_pos_provider pp = get_pos_provider();
     elaborator_context env = mk_elaborator_context(pp, check_unassigned);
-    auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
+    auto r = ::lean::elaborate(env, ctx, e, ensure_type);
     m_pre_info_manager.clear();
     return r;
 }
 
 std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<expr> const & ctx, bool clear_pre_info) {
-    bool relax            = false;
     bool check_unassigned = true;
     bool ensure_type      = true;
     parser_pos_provider pp = get_pos_provider();
     elaborator_context env = mk_elaborator_context(pp, check_unassigned);
-    auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
+    auto r = ::lean::elaborate(env, ctx, e, ensure_type);
     if (clear_pre_info)
         m_pre_info_manager.clear();
     return r;
 }
 
 std::tuple<expr, level_param_names> parser::elaborate_at(environment const & env, expr const & e) {
-    bool relax            = false;
     parser_pos_provider pp = get_pos_provider();
     elaborator_context eenv = mk_elaborator_context(env, pp);
-    auto r = ::lean::elaborate(eenv, list<expr>(), e, relax);
+    auto r = ::lean::elaborate(eenv, list<expr>(), e);
     m_pre_info_manager.clear();
     return r;
 }
 
-auto parser::elaborate_definition(name const & n, expr const & t, expr const & v,
-                                  bool is_opaque)
--> std::tuple<expr, expr, level_param_names> {
+auto parser::elaborate_definition(name const & n, expr const & t, expr const & v)
+    -> std::tuple<expr, expr, level_param_names> {
     parser_pos_provider pp = get_pos_provider();
     elaborator_context eenv = mk_elaborator_context(pp);
-    auto r = ::lean::elaborate(eenv, n, t, v, is_opaque);
+    auto r = ::lean::elaborate(eenv, n, t, v);
     m_pre_info_manager.clear();
     return r;
 }
 
 auto parser::elaborate_definition_at(environment const & env, local_level_decls const & lls,
-                                     name const & n, expr const & t, expr const & v, bool is_opaque)
+                                     name const & n, expr const & t, expr const & v)
 -> std::tuple<expr, expr, level_param_names> {
     parser_pos_provider pp = get_pos_provider();
     elaborator_context eenv = mk_elaborator_context(env, lls, pp);
-    auto r = ::lean::elaborate(eenv, n, t, v, is_opaque);
+    auto r = ::lean::elaborate(eenv, n, t, v);
     m_pre_info_manager.clear();
     return r;
 }
@@ -1639,7 +1634,7 @@ static optional<std::string> try_file(std::string const & base, optional<unsigne
 }
 
 static std::string * g_lua_module_key = nullptr;
-static void lua_module_reader(deserializer & d, module_idx, shared_environment &,
+static void lua_module_reader(deserializer & d, shared_environment &,
                               std::function<void(asynch_update_fn const &)> &,
                               std::function<void(delayed_update_fn const &)> & add_delayed_update) {
     name fname;
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 263868cdd..7b7976b49 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -477,10 +477,10 @@ public:
     /** \brief Elaborate \c e (making sure the result does not have metavariables). */
     std::tuple<expr, level_param_names> elaborate(expr const & e) { return elaborate_at(m_env, e); }
     /** \brief Elaborate the definition n : t := v */
-    std::tuple<expr, expr, level_param_names> elaborate_definition(name const & n, expr const & t, expr const & v, bool is_opaque);
+    std::tuple<expr, expr, level_param_names> elaborate_definition(name const & n, expr const & t, expr const & v);
     /** \brief Elaborate the definition n : t := v in the given environment*/
     std::tuple<expr, expr, level_param_names> elaborate_definition_at(environment const & env, local_level_decls const & lls,
-                                                                      name const & n, expr const & t, expr const & v, bool is_opaque);
+                                                                      name const & n, expr const & t, expr const & v);
 
     expr mk_sorry(pos_info const & p);
     bool used_sorry() const { return m_used_sorry; }
diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp
index f651da15b..d04b71514 100644
--- a/src/frontends/lean/server.cpp
+++ b/src/frontends/lean/server.cpp
@@ -767,7 +767,7 @@ bool match_type(type_checker & tc, expr const & meta, expr const & expected_type
         unifier_config cfg;
         cfg.m_max_steps = LEAN_FINDG_MAX_STEPS;
         cfg.m_kind      = unifier_kind::Cheap;
-        auto r = unify(tc.env(), dt, expected_type, tc.mk_ngen(), true, substitution(), cfg);
+        auto r = unify(tc.env(), dt, expected_type, tc.mk_ngen(), substitution(), cfg);
         return static_cast<bool>(r.pull());
     } catch (exception&) {
         return false;
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 46ac8b7bb..1c679825c 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -113,7 +113,7 @@ struct structure_cmd_fn {
     bool                        m_gen_proj_mk;
 
     structure_cmd_fn(parser & p):m_p(p), m_env(p.env()), m_ngen(p.mk_ngen()), m_namespace(get_namespace(m_env)) {
-        m_tc = mk_type_checker(m_env, m_p.mk_ngen(), false);
+        m_tc = mk_type_checker(m_env, m_p.mk_ngen());
         m_infer_result_universe = false;
         m_gen_eta     = get_structure_eta_thm(p.get_options());
         m_gen_proj_mk = get_structure_proj_mk_thm(p.get_options());
diff --git a/src/frontends/lean/theorem_queue.cpp b/src/frontends/lean/theorem_queue.cpp
index 385d31c63..dc91b1e38 100644
--- a/src/frontends/lean/theorem_queue.cpp
+++ b/src/frontends/lean/theorem_queue.cpp
@@ -18,8 +18,7 @@ void theorem_queue::add(environment const & env, name const & n, level_param_nam
     m_queue.add([=]() {
             level_param_names new_ls;
             expr type, value;
-            bool is_opaque = true; // theorems are always opaque
-            std::tie(type, value, new_ls) = m_parser.elaborate_definition_at(env, lls, n, t, v, is_opaque);
+            std::tie(type, value, new_ls) = m_parser.elaborate_definition_at(env, lls, n, t, v);
             new_ls = append(ls, new_ls);
             value  = expand_abbreviations(env, unfold_untrusted_macros(env, value));
             auto r = check(env, mk_theorem(n, new_ls, type, value));
diff --git a/src/kernel/constraint.cpp b/src/kernel/constraint.cpp
index 1067bbad7..95a299b81 100644
--- a/src/kernel/constraint.cpp
+++ b/src/kernel/constraint.cpp
@@ -16,22 +16,21 @@ struct constraint_cell {
     MK_LEAN_RC()
     constraint_kind m_kind;
     justification   m_jst;
-    bool            m_relax_main_opaque;
-    constraint_cell(constraint_kind k, justification const & j, bool relax):
-        m_rc(1), m_kind(k), m_jst(j), m_relax_main_opaque(relax) {}
+    constraint_cell(constraint_kind k, justification const & j):
+        m_rc(1), m_kind(k), m_jst(j) {}
 };
 struct eq_constraint_cell : public constraint_cell {
     expr m_lhs;
     expr m_rhs;
-    eq_constraint_cell(expr const & lhs, expr const & rhs, justification const & j, bool relax):
-        constraint_cell(constraint_kind::Eq, j, relax),
+    eq_constraint_cell(expr const & lhs, expr const & rhs, justification const & j):
+        constraint_cell(constraint_kind::Eq, j),
         m_lhs(lhs), m_rhs(rhs) {}
 };
 struct level_constraint_cell : public constraint_cell {
     level m_lhs;
     level m_rhs;
     level_constraint_cell(level const & lhs, level const & rhs, justification const & j):
-        constraint_cell(constraint_kind::LevelEq, j, false),
+        constraint_cell(constraint_kind::LevelEq, j),
         m_lhs(lhs), m_rhs(rhs) {}
 };
 struct choice_constraint_cell : public constraint_cell {
@@ -40,8 +39,8 @@ struct choice_constraint_cell : public constraint_cell {
     delay_factor m_delay_factor;
     bool         m_owner;
     choice_constraint_cell(expr const & e, choice_fn const & fn, delay_factor const & f,
-                           bool owner, justification const & j, bool relax):
-        constraint_cell(constraint_kind::Choice, j, relax),
+                           bool owner, justification const & j):
+        constraint_cell(constraint_kind::Choice, j),
         m_expr(e), m_fn(fn), m_delay_factor(f), m_owner(owner) {}
 };
 
@@ -65,16 +64,16 @@ constraint & constraint::operator=(constraint && c) { LEAN_MOVE_REF(c); }
 constraint_kind constraint::kind() const { lean_assert(m_ptr); return m_ptr->m_kind; }
 justification const & constraint::get_justification() const { lean_assert(m_ptr); return m_ptr->m_jst; }
 
-constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque) {
-    return constraint(new eq_constraint_cell(lhs, rhs, j, relax_main_opaque));
+constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
+    return constraint(new eq_constraint_cell(lhs, rhs, j));
 }
 constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j) {
     return constraint(new level_constraint_cell(lhs, rhs, j));
 }
 constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, delay_factor const & f,
-                           bool owner, justification const & j, bool relax_main_opaque) {
+                           bool owner, justification const & j) {
     lean_assert(is_meta(m));
-    return constraint(new choice_constraint_cell(m, fn, f, owner, j, relax_main_opaque));
+    return constraint(new choice_constraint_cell(m, fn, f, owner, j));
 }
 
 expr const & cnstr_lhs_expr(constraint const & c) {
@@ -85,7 +84,6 @@ expr const & cnstr_rhs_expr(constraint const & c) {
     lean_assert(is_eq_cnstr(c));
     return static_cast<eq_constraint_cell*>(c.raw())->m_rhs;
 }
-bool relax_main_opaque(constraint const & c) { return c.raw()->m_relax_main_opaque; }
 level const & cnstr_lhs_level(constraint const & c) {
     lean_assert(is_level_eq_cnstr(c));
     return static_cast<level_constraint_cell*>(c.raw())->m_lhs;
@@ -119,13 +117,13 @@ bool cnstr_is_owner(constraint const & c) {
 constraint update_justification(constraint const & c, justification const & j) {
     switch (c.kind()) {
     case constraint_kind::Eq:
-        return mk_eq_cnstr(cnstr_lhs_expr(c), cnstr_rhs_expr(c), j, relax_main_opaque(c));
+        return mk_eq_cnstr(cnstr_lhs_expr(c), cnstr_rhs_expr(c), j);
     case constraint_kind::LevelEq:
         return mk_level_eq_cnstr(cnstr_lhs_level(c), cnstr_rhs_level(c), j);
     case constraint_kind::Choice:
         return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c),
                                static_cast<choice_constraint_cell*>(c.raw())->m_delay_factor,
-                               cnstr_is_owner(c), j, relax_main_opaque(c));
+                               cnstr_is_owner(c), j);
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
diff --git a/src/kernel/constraint.h b/src/kernel/constraint.h
index aa38e4529..e6fc68e03 100644
--- a/src/kernel/constraint.h
+++ b/src/kernel/constraint.h
@@ -77,10 +77,10 @@ public:
     friend bool is_eqp(constraint const & c1, constraint const & c2) { return c1.m_ptr == c2.m_ptr; }
     friend void swap(constraint & l1, constraint & l2) { std::swap(l1, l2); }
 
-    friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque);
+    friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
     friend constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j);
     friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, delay_factor const & f, bool owner,
-                                      justification const & j, bool relax_main_opaque);
+                                      justification const & j);
 
     constraint_cell * raw() const { return m_ptr; }
 };
@@ -88,10 +88,8 @@ public:
 inline bool operator==(constraint const & c1, constraint const & c2) { return c1.raw() == c2.raw(); }
 inline bool operator!=(constraint const & c1, constraint const & c2) { return !(c1 == c2); }
 
-/** \brief Create a unification constraint lhs =?= rhs
-    If \c relax_main_opaque is true, then opaque definitions from the main module are treated as transparent.
-*/
-constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque);
+/** \brief Create a unification constraint lhs =?= rhs */
+constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j);
 constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j);
 
 /** \brief Create a "choice" constraint m in fn(...), where fn produces a stream of possible solutions.
@@ -100,11 +98,9 @@ constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification
     The variable will be assigned by the choice constraint, and the elaborator should just check whether a solution
     produced by fn satisfies the other constraints or not.
     \c j is a justification for the constraint.
-    If \c relax_main_opaque is true, then it signs that constraint was created in a context where
-    opaque constants of the main module can be treated as transparent.
 */
 constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, delay_factor const & f,
-                           bool owner, justification const & j, bool relax_main_opaque);
+                           bool owner, justification const & j);
 
 inline bool is_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::Eq; }
 inline bool is_level_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::LevelEq; }
@@ -116,8 +112,6 @@ constraint update_justification(constraint const & c, justification const & j);
 expr const & cnstr_lhs_expr(constraint const & c);
 /** \brief Return the rhs of an equality constraint. */
 expr const & cnstr_rhs_expr(constraint const & c);
-/** \brief Return true iff opaque definitions from the main module should be treated as transparent. */
-bool relax_main_opaque(constraint const & c);
 /** \brief Return the lhs of an level constraint. */
 level const & cnstr_lhs_level(constraint const & c);
 /** \brief Return the rhs of an level constraint. */
diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp
index d6b636763..ad01f0077 100644
--- a/src/kernel/converter.cpp
+++ b/src/kernel/converter.cpp
@@ -35,7 +35,6 @@ struct dummy_converter : public converter {
     virtual pair<bool, constraint_seq> is_def_eq(expr const &, expr const &, type_checker &, delayed_justification &) {
         return mk_pair(true, constraint_seq());
     }
-    virtual optional<module_idx> get_module_idx() const { return optional<module_idx>(); }
     virtual bool is_opaque(declaration const &) const { return false; }
     virtual optional<declaration> is_delta(expr const &) const { return optional<declaration>(); }
     virtual bool is_stuck(expr const &, type_checker &) { return false; }
diff --git a/src/kernel/converter.h b/src/kernel/converter.h
index e66a23f54..7c9338b11 100644
--- a/src/kernel/converter.h
+++ b/src/kernel/converter.h
@@ -18,7 +18,6 @@ protected:
     extension_context & get_extension(type_checker & tc);
 public:
     virtual ~converter() {}
-    virtual optional<module_idx> get_module_idx() const = 0;
     virtual bool is_opaque(declaration const & d) const = 0;
     virtual optional<declaration> is_delta(expr const & e) const = 0;
 
diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp
index 95a5c8626..ff21d69ea 100644
--- a/src/kernel/declaration.cpp
+++ b/src/kernel/declaration.cpp
@@ -18,7 +18,6 @@ struct declaration::cell {
     optional<expr>    m_value;        // if none, then declaration is actually a postulate
     // The following fields are only meaningful for definitions (which are not theorems)
     unsigned          m_weight;
-    unsigned          m_module_idx;   // module idx where it was defined
     bool              m_opaque;
     // The following field affects the convertability checker.
     // Let f be this definition, then if the following field is true,
@@ -31,11 +30,11 @@ struct declaration::cell {
 
     cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom):
         m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom),
-        m_weight(0), m_module_idx(0), m_opaque(true), m_use_conv_opt(false) {}
+        m_weight(0), m_opaque(true), m_use_conv_opt(false) {}
     cell(name const & n, level_param_names const & params, expr const & t, bool is_thm, expr const & v,
-         bool opaque, unsigned w, module_idx mod_idx, bool use_conv_opt):
+         bool opaque, unsigned w, bool use_conv_opt):
         m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm),
-        m_value(v), m_weight(w), m_module_idx(mod_idx), m_opaque(opaque), m_use_conv_opt(use_conv_opt) {}
+        m_value(v), m_weight(w), m_opaque(opaque), m_use_conv_opt(use_conv_opt) {}
 };
 
 static declaration * g_dummy = nullptr;
@@ -62,15 +61,14 @@ expr const & declaration::get_type() const { return m_ptr->m_type; }
 bool declaration::is_opaque() const { return m_ptr->m_opaque; }
 expr const & declaration::get_value() const { lean_assert(is_definition()); return *(m_ptr->m_value); }
 unsigned declaration::get_weight() const { return m_ptr->m_weight; }
-module_idx declaration::get_module_idx() const { return m_ptr->m_module_idx; }
 bool declaration::use_conv_opt() const { return m_ptr->m_use_conv_opt; }
 
 declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
-                          bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt) {
-    return declaration(new declaration::cell(n, params, t, false, v, opaque, weight, mod_idx, use_conv_opt));
+                          bool opaque, unsigned weight, bool use_conv_opt) {
+    return declaration(new declaration::cell(n, params, t, false, v, opaque, weight, use_conv_opt));
 }
 declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
-                          bool opaque, module_idx mod_idx, bool use_conv_opt) {
+                          bool opaque, bool use_conv_opt) {
     unsigned w = 0;
     for_each(v, [&](expr const & e, unsigned) {
             if (is_constant(e)) {
@@ -80,10 +78,10 @@ declaration mk_definition(environment const & env, name const & n, level_param_n
             }
             return true;
         });
-    return mk_definition(n, params, t, v, opaque, w+1, mod_idx, use_conv_opt);
+    return mk_definition(n, params, t, v, opaque, w+1, use_conv_opt);
 }
-declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, module_idx mod_idx) {
-    return declaration(new declaration::cell(n, params, t, true, v, true, 0, mod_idx, false));
+declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) {
+    return declaration(new declaration::cell(n, params, t, true, v, true, 0, false));
 }
 declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) {
     return declaration(new declaration::cell(n, params, t, true));
diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h
index 360d9e5ad..b1c8de13a 100644
--- a/src/kernel/declaration.h
+++ b/src/kernel/declaration.h
@@ -12,21 +12,6 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 
 namespace lean {
-/**
-    \brief Module index. The kernel provides only basic support
-    for implementing a module system outside of the kernel.
-
-    We need at least the notion of module index in the kernel, because
-    it affects the convertability procedure.
-
-    Given an opaque definition (non-theorem) d in module m1, then d is considered
-    to be transparent for any other opaque definition in module m1.
-*/
-typedef unsigned module_idx;
-/** \brief The main module is the module being currently compiled. We always assigned it the index 0. */
-constexpr module_idx g_main_module_idx = 0;
-constexpr module_idx g_null_module_idx = std::numeric_limits<unsigned>::max();
-
 /** \brief Environment definitions, theorems, axioms and variable declarations. */
 class declaration {
     struct cell;
@@ -67,14 +52,13 @@ public:
     expr const & get_value() const;
     bool is_opaque() const;
     unsigned get_weight() const;
-    module_idx get_module_idx() const;
     bool use_conv_opt() const;
 
     friend declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t,
-                                    expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt);
+                                    expr const & v, bool opaque, bool use_conv_opt);
     friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, bool opaque,
-                                    unsigned weight, module_idx mod_idx, bool use_conv_opt);
-    friend declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, module_idx mod_idx);
+                                    unsigned weight, bool use_conv_opt);
+    friend declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
     friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
     friend declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t);
 };
@@ -84,10 +68,10 @@ inline optional<declaration> some_declaration(declaration const & o) { return op
 inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); }
 
 declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
-                         bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true);
+                         bool opaque = false, unsigned weight = 0, bool use_conv_opt = true);
 declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
-                         bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true);
-declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, module_idx mod_idx = 0);
+                         bool opaque = false, bool use_conv_opt = true);
+declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
 declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
 declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t);
 
diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp
index 7afb60002..3d66840a7 100644
--- a/src/kernel/default_converter.cpp
+++ b/src/kernel/default_converter.cpp
@@ -14,17 +14,14 @@ Author: Leonardo de Moura
 namespace lean {
 static expr * g_dont_care = nullptr;
 
-default_converter::default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize):
-    m_env(env), m_module_idx(mod_idx), m_memoize(memoize) {
+default_converter::default_converter(environment const & env, bool memoize):
+    m_env(env), m_memoize(memoize) {
     m_tc  = nullptr;
     m_jst = nullptr;
 }
 
-default_converter::default_converter(environment const & env, bool relax_main_opaque, bool memoize):
-    default_converter(env, relax_main_opaque ? optional<module_idx>(0) : optional<module_idx>(), memoize) {}
-
 constraint default_converter::mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
-    return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast<bool>(m_module_idx));
+    return ::lean::mk_eq_cnstr(lhs, rhs, j);
 }
 
 optional<expr> default_converter::expand_macro(expr const & m) {
@@ -115,7 +112,6 @@ bool default_converter::is_opaque(declaration const & d) const {
     lean_assert(d.is_definition());
     if (d.is_theorem()) return true;                               // theorems are always opaque
     if (!d.is_opaque()) return false;                              // d is a transparent definition
-    if (m_module_idx && d.get_module_idx() == *m_module_idx) return false; // the opaque definitions in mod_idx are considered transparent
     return true;                                                   // d is opaque
 }
 
diff --git a/src/kernel/default_converter.h b/src/kernel/default_converter.h
index 8992d672c..2300645e2 100644
--- a/src/kernel/default_converter.h
+++ b/src/kernel/default_converter.h
@@ -17,7 +17,6 @@ namespace lean {
 class default_converter : public converter {
 protected:
     environment                                 m_env;
-    optional<module_idx>                        m_module_idx;
     bool                                        m_memoize;
     expr_struct_map<expr>                       m_whnf_core_cache;
     expr_struct_map<pair<expr, constraint_seq>> m_whnf_cache;
@@ -73,12 +72,10 @@ protected:
     pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s);
 
 public:
-    default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize = true);
-    default_converter(environment const & env, bool relax_main_opaque, bool memoize = true);
+    default_converter(environment const & env, bool memoize = true);
 
     virtual optional<declaration> is_delta(expr const & e) const;
     virtual bool is_opaque(declaration const & d) const;
-    virtual optional<module_idx> get_module_idx() const { return m_module_idx; }
 
     virtual bool is_stuck(expr const & e, type_checker & c);
     virtual pair<expr, constraint_seq> whnf(expr const & e_prime, type_checker & c);
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 2a8e682a9..432be973d 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -85,7 +85,7 @@ pair<expr, expr> type_checker::open_binding_body(expr const & e) {
 }
 
 constraint type_checker::mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
-    return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast<bool>(m_conv->get_module_idx()));
+    return ::lean::mk_eq_cnstr(lhs, rhs, j);
 }
 
 /**
@@ -422,12 +422,12 @@ type_checker::type_checker(environment const & env, name_generator const & g, st
 }
 
 type_checker::type_checker(environment const & env, name_generator const & g, bool memoize):
-    type_checker(env, g, std::unique_ptr<converter>(new default_converter(env, optional<module_idx>(), memoize)), memoize) {}
+    type_checker(env, g, std::unique_ptr<converter>(new default_converter(env, memoize)), memoize) {}
 
 static name * g_tmp_prefix = nullptr;
 
 type_checker::type_checker(environment const & env):
-    type_checker(env, name_generator(*g_tmp_prefix), std::unique_ptr<converter>(new default_converter(env, optional<module_idx>())), true) {}
+    type_checker(env, name_generator(*g_tmp_prefix), std::unique_ptr<converter>(new default_converter(env)), true) {}
 
 type_checker::~type_checker() {}
 
@@ -479,14 +479,11 @@ certified_declaration check(environment const & env, declaration const & d, name
     check_name(env, d.get_name());
     check_duplicated_params(env, d);
     bool memoize = true;
-    type_checker checker1(env, g, std::unique_ptr<converter>(new default_converter(env, optional<module_idx>(), memoize)));
+    type_checker checker1(env, g, std::unique_ptr<converter>(new default_converter(env, memoize)));
     expr sort = checker1.check(d.get_type(), d.get_univ_params()).first;
     checker1.ensure_sort(sort, d.get_type());
     if (d.is_definition()) {
-        optional<module_idx> midx;
-        if (d.is_opaque())
-            midx = optional<module_idx>(d.get_module_idx());
-        type_checker checker2(env, g, std::unique_ptr<converter>(new default_converter(env, midx, memoize)));
+        type_checker checker2(env, g, std::unique_ptr<converter>(new default_converter(env, memoize)));
         expr val_type = checker2.check(d.get_value(), d.get_univ_params()).first;
         if (!checker2.is_def_eq(val_type, d.get_type()).first) {
             throw_kernel_exception(env, d.get_value(), [=](formatter const & fmt) {
diff --git a/src/library/class.cpp b/src/library/class.cpp
index 38ba73d0c..719a2662b 100644
--- a/src/library/class.cpp
+++ b/src/library/class.cpp
@@ -187,7 +187,7 @@ environment add_instance(environment const & env, name const & n, unsigned prior
     declaration d = env.get(n);
     expr type = d.get_type();
     name_generator ngen(*g_tmp_prefix);
-    auto tc = mk_type_checker(env, ngen, false);
+    auto tc = mk_type_checker(env, ngen);
     while (true) {
         type = tc->whnf(type).first;
         if (!is_pi(type))
diff --git a/src/library/definitional/brec_on.cpp b/src/library/definitional/brec_on.cpp
index 8071f4d3e..153ff1ed4 100644
--- a/src/library/definitional/brec_on.cpp
+++ b/src/library/definitional/brec_on.cpp
@@ -144,7 +144,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
     bool opaque       = false;
     bool use_conv_opt = true;
     declaration new_d = mk_definition(env, below_name, blvls, below_type, below_value,
-                                      opaque, rec_decl.get_module_idx(), use_conv_opt);
+                                      opaque, use_conv_opt);
     environment new_env = module::add(env, check(env, new_d));
     new_env = set_reducible(new_env, below_name, reducible_status::Reducible);
     if (!ibelow)
@@ -331,7 +331,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
     bool opaque       = false;
     bool use_conv_opt = true;
     declaration new_d = mk_definition(env, brec_on_name, blps, brec_on_type, brec_on_value,
-                                      opaque, rec_decl.get_module_idx(), use_conv_opt);
+                                      opaque, use_conv_opt);
     environment new_env = module::add(env, check(env, new_d));
     new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible);
     if (!ind)
diff --git a/src/library/definitional/cases_on.cpp b/src/library/definitional/cases_on.cpp
index f071d0bfe..3f353bcac 100644
--- a/src/library/definitional/cases_on.cpp
+++ b/src/library/definitional/cases_on.cpp
@@ -180,7 +180,7 @@ environment mk_cases_on(environment const & env, name const & n) {
     bool opaque       = false;
     bool use_conv_opt = true;
     declaration new_d = mk_definition(env, cases_on_name, rec_decl.get_univ_params(), cases_on_type, cases_on_value,
-                                      opaque, rec_decl.get_module_idx(), use_conv_opt);
+                                      opaque, use_conv_opt);
     environment new_env = module::add(env, check(env, new_d));
     new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible);
     new_env = add_unfold_c_hint(new_env, cases_on_name, cases_on_major_idx);
diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp
index 54ccef046..f1754130e 100644
--- a/src/library/definitional/equations.cpp
+++ b/src/library/definitional/equations.cpp
@@ -1721,8 +1721,7 @@ class equation_compiler_fn {
 
 
 public:
-    equation_compiler_fn(type_checker & tc, io_state const & ios, expr const & meta, expr const & meta_type,
-                         bool /* relax */):
+    equation_compiler_fn(type_checker & tc, io_state const & ios, expr const & meta, expr const & meta_type):
         m_tc(tc), m_ios(ios), m_meta(meta), m_meta_type(meta_type) {
         get_app_args(m_meta, m_global_context);
     }
@@ -1746,7 +1745,7 @@ public:
 };
 
 expr compile_equations(type_checker & tc, io_state const & ios, expr const & eqns,
-                       expr const & meta, expr const & meta_type, bool relax) {
-    return equation_compiler_fn(tc, ios, meta, meta_type, relax)(eqns);
+                       expr const & meta, expr const & meta_type) {
+    return equation_compiler_fn(tc, ios, meta, meta_type)(eqns);
 }
 }
diff --git a/src/library/definitional/equations.h b/src/library/definitional/equations.h
index 6bd439efe..1096cefa7 100644
--- a/src/library/definitional/equations.h
+++ b/src/library/definitional/equations.h
@@ -42,7 +42,7 @@ expr mk_inaccessible(expr const & e);
 bool is_inaccessible(expr const & e);
 
 expr compile_equations(type_checker & tc, io_state const & ios, expr const & eqns,
-                       expr const & meta, expr const & meta_type, bool relax);
+                       expr const & meta, expr const & meta_type);
 
 /** \brief Return true if \c e is an auxiliary macro used to store the result of mutually recursive declarations.
     For example, if a set of recursive equations is defining \c n mutually recursive functions, we wrap
diff --git a/src/library/definitional/induction_on.cpp b/src/library/definitional/induction_on.cpp
index 6f46fa629..33a8ee26c 100644
--- a/src/library/definitional/induction_on.cpp
+++ b/src/library/definitional/induction_on.cpp
@@ -32,7 +32,7 @@ environment mk_induction_on(environment const & env, name const & n) {
         certified_declaration cdecl = check(new_env,
                                             mk_definition(new_env, induction_on_name, rec_on_decl.get_univ_params(),
                                                           rec_on_decl.get_type(), rec_on_decl.get_value(),
-                                                          opaque, rec_on_decl.get_module_idx(), use_conv_opt));
+                                                          opaque, use_conv_opt));
         new_env = module::add(new_env, cdecl);
     } else {
         level_param_names induction_on_univs = tail(rec_on_decl.get_univ_params());
@@ -43,7 +43,7 @@ environment mk_induction_on(environment const & env, name const & n) {
         certified_declaration cdecl = check(new_env,
                                             mk_definition(new_env, induction_on_name, induction_on_univs,
                                                           induction_on_type, induction_on_value,
-                                                          opaque, rec_on_decl.get_module_idx(), use_conv_opt));
+                                                          opaque, use_conv_opt));
         new_env = module::add(new_env, cdecl);
     }
     return add_protected(new_env, induction_on_name);
diff --git a/src/library/definitional/no_confusion.cpp b/src/library/definitional/no_confusion.cpp
index ebba06f6a..781ea825c 100644
--- a/src/library/definitional/no_confusion.cpp
+++ b/src/library/definitional/no_confusion.cpp
@@ -137,7 +137,7 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
     bool opaque       = false;
     bool use_conv_opt = true;
     declaration new_d = mk_definition(env, no_confusion_type_name, lps, no_confusion_type_type, no_confusion_type_value,
-                                      opaque, ind_decl.get_module_idx(), use_conv_opt);
+                                      opaque, use_conv_opt);
     environment new_env = module::add(env, check(env, new_d));
     new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::Reducible);
     return some(add_protected(new_env, no_confusion_type_name));
@@ -272,7 +272,7 @@ environment mk_no_confusion(environment const & env, name const & n) {
     bool opaque       = false;
     bool use_conv_opt = true;
     declaration new_d = mk_definition(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val,
-                                      opaque, no_confusion_type_decl.get_module_idx(), use_conv_opt);
+                                      opaque, use_conv_opt);
     new_env = module::add(new_env, check(new_env, new_d));
     new_env = set_reducible(new_env, no_confusion_name, reducible_status::Reducible);
     return add_protected(new_env, no_confusion_name);
diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp
index 707f5c5d7..1b2f64ed6 100644
--- a/src/library/definitional/projection.cpp
+++ b/src/library/definitional/projection.cpp
@@ -132,7 +132,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         bool opaque       = false;
         bool use_conv_opt = false;
         declaration new_d = mk_definition(env, proj_name, lvl_params, proj_type, proj_val,
-                                          opaque, rec_decl.get_module_idx(), use_conv_opt);
+                                          opaque, use_conv_opt);
         new_env = module::add(new_env, check(new_env, new_d));
         new_env = set_reducible(new_env, proj_name, reducible_status::Reducible);
         new_env = add_unfold_c_hint(new_env, proj_name, nparams);
diff --git a/src/library/definitional/rec_on.cpp b/src/library/definitional/rec_on.cpp
index 427be56d4..f4df0c84a 100644
--- a/src/library/definitional/rec_on.cpp
+++ b/src/library/definitional/rec_on.cpp
@@ -58,7 +58,7 @@ environment mk_rec_on(environment const & env, name const & n) {
     environment new_env = module::add(env,
                                       check(env, mk_definition(env, rec_on_name, rec_decl.get_univ_params(),
                                                                rec_on_type, rec_on_val,
-                                                               opaque, rec_decl.get_module_idx(), use_conv_opt)));
+                                                               opaque, use_conv_opt)));
     new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible);
     new_env = add_unfold_c_hint(new_env, rec_on_name, rec_on_major_idx);
     return add_protected(new_env, rec_on_name);
diff --git a/src/library/inductive_unifier_plugin.cpp b/src/library/inductive_unifier_plugin.cpp
index 5d76c96a5..63d715376 100644
--- a/src/library/inductive_unifier_plugin.cpp
+++ b/src/library/inductive_unifier_plugin.cpp
@@ -45,7 +45,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
     */
     lazy_list<constraints> add_elim_meta_cnstrs(type_checker & tc, name_generator ngen, inductive::inductive_decl const & decl,
                                                 expr const & elim, buffer<expr> & args, expr const & t, justification const & j,
-                                                constraint_seq cs, bool relax) const {
+                                                constraint_seq cs) const {
         lean_assert(is_constant(elim));
         environment const & env = tc.env();
         levels elim_lvls       = const_levels(elim);
@@ -75,10 +75,10 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
                 hint = mk_app(hint, mk_app(mk_aux_metavar_for(ngen, mtype), margs));
                 intro_type = tc.whnf(binding_body(intro_type), cs_intro);
             }
-            constraint c1      = mk_eq_cnstr(meta, hint, j, relax);
+            constraint c1      = mk_eq_cnstr(meta, hint, j);
             args[major_idx]    = hint;
             expr reduce_elim   = tc.whnf(mk_app(elim, args), cs_intro);
-            constraint c2      = mk_eq_cnstr(reduce_elim, t, j, relax);
+            constraint c2      = mk_eq_cnstr(reduce_elim, t, j);
             cs_intro = constraint_seq(c1) + constraint_seq(c2) + cs_intro;
             buffer<constraint> cs_buffer;
             cs_intro.linearize(cs_buffer);
@@ -88,7 +88,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
     }
 
     lazy_list<constraints> process_elim_meta_core(type_checker & tc, name_generator const & ngen,
-                                                  expr const & lhs, expr const & rhs, justification const & j, bool relax) const {
+                                                  expr const & lhs, expr const & rhs, justification const & j) const {
         lean_assert(inductive::is_elim_meta_app(tc, lhs));
         auto dcs = tc.is_def_eq_types(lhs, rhs, j);
         if (!dcs.first)
@@ -101,7 +101,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
         auto decls   = *inductive::is_inductive_decl(env, it_name);
         for (auto const & d : std::get<2>(decls)) {
             if (inductive::inductive_decl_name(d) == it_name)
-                return add_elim_meta_cnstrs(tc, ngen, d, elim, args, rhs, j, cs, relax);
+                return add_elim_meta_cnstrs(tc, ngen, d, elim, args, rhs, j, cs);
         }
         lean_unreachable(); // LCOV_EXCL_LINE
     }
@@ -117,11 +117,10 @@ public:
         expr const & lhs        = cnstr_lhs_expr(c);
         expr const & rhs        = cnstr_rhs_expr(c);
         justification const & j = c.get_justification();
-        bool relax = relax_main_opaque(c);
         if (inductive::is_elim_meta_app(tc, lhs))
-            return process_elim_meta_core(tc, ngen, lhs, rhs, j, relax);
+            return process_elim_meta_core(tc, ngen, lhs, rhs, j);
         else if (inductive::is_elim_meta_app(tc, rhs))
-            return process_elim_meta_core(tc, ngen, rhs, lhs, j, relax);
+            return process_elim_meta_core(tc, ngen, rhs, lhs, j);
         else
             return lazy_list<constraints>();
     }
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index 677b3c035..3072978fd 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -753,7 +753,6 @@ static int declaration_get_value(lua_State * L) {
     throw exception("arg #1 must be a definition");
 }
 static int declaration_get_weight(lua_State * L) { return push_integer(L, to_declaration(L, 1).get_weight()); }
-static int declaration_get_module_idx(lua_State * L) { return push_integer(L, to_declaration(L, 1).get_module_idx()); }
 static int mk_constant_assumption(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 2)
@@ -775,38 +774,37 @@ static int mk_theorem(lua_State * L) {
     else
         return push_declaration(L, mk_theorem(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3), to_expr(L, 4)));
 }
-static void get_definition_args(lua_State * L, int idx, bool & opaque, unsigned & weight, module_idx & mod_idx, bool & use_conv_opt) {
+static void get_definition_args(lua_State * L, int idx, bool & opaque, unsigned & weight, bool & use_conv_opt) {
     opaque       = get_bool_named_param(L, idx, "opaque", opaque);
     use_conv_opt = get_bool_named_param(L, idx, "use_conv_opt", use_conv_opt);
-    mod_idx      = get_uint_named_param(L, idx, "module_idx", mod_idx);
     weight       = get_uint_named_param(L, idx, "weight", weight);
 }
 static int mk_definition(lua_State * L) {
     int nargs = lua_gettop(L);
-    bool opaque = true; unsigned weight = 0; module_idx mod_idx = 0; bool use_conv_opt = true;
+    bool opaque = false; unsigned weight = 0; bool use_conv_opt = true;
     if (nargs < 3) {
         throw exception("mk_definition must have at least 3 arguments");
     } else if (is_environment(L, 1)) {
         if (nargs < 4) {
             throw exception("mk_definition must have at least 4 arguments, when the first argument is an environment");
         } else if (is_expr(L, 3)) {
-            get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt);
+            get_definition_args(L, 5, opaque, weight, use_conv_opt);
             return push_declaration(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), level_param_names(),
-                                                    to_expr(L, 3), to_expr(L, 4), opaque, mod_idx, use_conv_opt));
+                                                    to_expr(L, 3), to_expr(L, 4), opaque, use_conv_opt));
         } else {
-            get_definition_args(L, 6, opaque, weight, mod_idx, use_conv_opt);
+            get_definition_args(L, 6, opaque, weight, use_conv_opt);
             return push_declaration(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_level_param_names(L, 3),
-                                                    to_expr(L, 4), to_expr(L, 5), opaque, mod_idx, use_conv_opt));
+                                                    to_expr(L, 4), to_expr(L, 5), opaque, use_conv_opt));
         }
     } else {
         if (is_expr(L, 2)) {
-            get_definition_args(L, 4, opaque, weight, mod_idx, use_conv_opt);
+            get_definition_args(L, 4, opaque, weight, use_conv_opt);
             return push_declaration(L, mk_definition(to_name_ext(L, 1), level_param_names(), to_expr(L, 2),
-                                                    to_expr(L, 3), opaque, weight, mod_idx, use_conv_opt));
+                                                    to_expr(L, 3), opaque, weight, use_conv_opt));
         } else {
-            get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt);
+            get_definition_args(L, 5, opaque, weight, use_conv_opt);
             return push_declaration(L, mk_definition(to_name_ext(L, 1), to_level_param_names(L, 2),
-                                                    to_expr(L, 3), to_expr(L, 4), opaque, weight, mod_idx, use_conv_opt));
+                                                    to_expr(L, 3), to_expr(L, 4), opaque, weight, use_conv_opt));
         }
     }
 }
@@ -824,7 +822,6 @@ static const struct luaL_Reg declaration_m[] = {
     {"type",             safe_function<declaration_get_type>},
     {"value",            safe_function<declaration_get_value>},
     {"weight",           safe_function<declaration_get_weight>},
-    {"module_idx",       safe_function<declaration_get_module_idx>},
     {0, 0}
 };
 
@@ -1481,8 +1478,7 @@ static int constraint_tostring(lua_State * L) {
 static int mk_eq_cnstr(lua_State * L) {
     int nargs = lua_gettop(L);
     return push_constraint(L, mk_eq_cnstr(to_expr(L, 1), to_expr(L, 2),
-                                          nargs >= 3 ? to_justification(L, 3) : justification(),
-                                          nargs >= 4 && lua_toboolean(L, 4)));
+                                          nargs >= 3 ? to_justification(L, 3) : justification()));
 }
 static int mk_level_eq_cnstr(lua_State * L) {
     int nargs = lua_gettop(L);
@@ -1512,7 +1508,7 @@ static choice_fn to_choice_fn(lua_State * L, int idx) {
                     if (is_constraint(L, -1))
                         r.push_back(constraints(to_constraint(L, -1)));
                     else if (is_expr(L, -1))
-                        r.push_back(constraints(mk_eq_cnstr(mvar, to_expr(L, -1), justification(), false)));
+                        r.push_back(constraints(mk_eq_cnstr(mvar, to_expr(L, -1), justification())));
                     else
                         r.push_back(to_list_constraint_ext(L, -1));
                     lua_pop(L, 1);
@@ -1530,19 +1526,16 @@ static int mk_choice_cnstr(lua_State * L) {
     expr m           = to_expr(L, 1);
     choice_fn fn     = to_choice_fn(L, 2);
     if (nargs == 2)
-        return push_constraint(L, mk_choice_cnstr(m, fn, 0, false, justification(), false));
+        return push_constraint(L, mk_choice_cnstr(m, fn, 0, false, justification()));
     else if (nargs == 3 && is_justification(L, 3))
-        return push_constraint(L, mk_choice_cnstr(m, fn, 0, false, to_justification(L, 3), false));
+        return push_constraint(L, mk_choice_cnstr(m, fn, 0, false, to_justification(L, 3)));
     else if (nargs == 3)
-        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), false, justification(), false));
+        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), false, justification()));
     else if (nargs == 4)
-        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), lua_toboolean(L, 4), justification(), false));
-    else if (nargs == 5)
-        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), lua_toboolean(L, 4),
-                                                  to_justification(L, 5), false));
+        return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), lua_toboolean(L, 4), justification()));
     else
         return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), lua_toboolean(L, 4),
-                                                  to_justification(L, 5), lua_toboolean(L, 6)));
+                                                  to_justification(L, 5)));
 }
 
 static int constraint_expr(lua_State * L) {
@@ -1796,13 +1789,9 @@ static int mk_type_checker_with_hints(lua_State * L) {
     environment const & env = to_environment(L, 1);
     int nargs = lua_gettop(L);
     if (nargs == 1) {
-        return push_type_checker_ref(L, mk_type_checker(env, name_generator(*g_tmp_prefix), false));
-    } else if (nargs == 2 && lua_isboolean(L, 2)) {
-        return push_type_checker_ref(L, mk_type_checker(env, name_generator(*g_tmp_prefix), lua_toboolean(L, 2)));
-    } else if (nargs == 2) {
-        return push_type_checker_ref(L, mk_type_checker(env, to_name_generator(L, 2), false));
+        return push_type_checker_ref(L, mk_type_checker(env, name_generator(*g_tmp_prefix)));
     } else {
-        return push_type_checker_ref(L, mk_type_checker(env, to_name_generator(L, 2), lua_toboolean(L, 3)));
+        return push_type_checker_ref(L, mk_type_checker(env, to_name_generator(L, 2)));
     }
 }
 
diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp
index be991ef82..8d3a286f5 100644
--- a/src/library/kernel_serializer.cpp
+++ b/src/library/kernel_serializer.cpp
@@ -298,7 +298,7 @@ serializer & operator<<(serializer & s, declaration const & d) {
     return s;
 }
 
-declaration read_declaration(deserializer & d, module_idx midx) {
+declaration read_declaration(deserializer & d) {
     char k               = d.read_char();
     bool has_value       = (k & 1) != 0;
     bool is_th_ax        = (k & 8) != 0;
@@ -308,12 +308,12 @@ declaration read_declaration(deserializer & d, module_idx midx) {
     if (has_value) {
         expr v      = read_expr(d);
         if (is_th_ax) {
-            return mk_theorem(n, ps, t, v, midx);
+            return mk_theorem(n, ps, t, v);
         } else {
             unsigned w        = d.read_unsigned();
             bool is_opaque    = (k & 2) != 0;
             bool use_conv_opt = (k & 4) != 0;
-            return mk_definition(n, ps, t, v, is_opaque, w, midx, use_conv_opt);
+            return mk_definition(n, ps, t, v, is_opaque, w, use_conv_opt);
         }
     } else {
         if (is_th_ax)
diff --git a/src/library/kernel_serializer.h b/src/library/kernel_serializer.h
index 31c2b724d..9111016cd 100644
--- a/src/library/kernel_serializer.h
+++ b/src/library/kernel_serializer.h
@@ -27,7 +27,7 @@ expr read_expr(deserializer & d);
 inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d); return d; }
 
 serializer & operator<<(serializer & s, declaration const & d);
-declaration read_declaration(deserializer & d, module_idx midx);
+declaration read_declaration(deserializer & d);
 
 typedef std::tuple<level_param_names, unsigned, list<inductive::inductive_decl>> inductive_decls;
 serializer & operator<<(serializer & s, inductive_decls const & ds);
diff --git a/src/library/metavar_closure.cpp b/src/library/metavar_closure.cpp
index 09f54a6bb..ab79b9aa2 100644
--- a/src/library/metavar_closure.cpp
+++ b/src/library/metavar_closure.cpp
@@ -45,10 +45,10 @@ void metavar_closure::for_each_level_mvar(std::function<void(level const &)> con
     m_lvl_mvars.for_each(fn);
 }
 
-void metavar_closure::mk_constraints(substitution s, justification const & j, bool relax, buffer<constraint> & r) const {
+void metavar_closure::mk_constraints(substitution s, justification const & j, buffer<constraint> & r) const {
     m_expr_mvars.for_each([&](expr const & m) {
             if (s.is_expr_assigned(mlocal_name(m)))
-                r.push_back(mk_eq_cnstr(m, s.instantiate(m), j, relax));
+                r.push_back(mk_eq_cnstr(m, s.instantiate(m), j));
         });
     m_lvl_mvars.for_each([&](level const & m) {
             if (s.is_level_assigned(meta_id(m)))
@@ -56,9 +56,9 @@ void metavar_closure::mk_constraints(substitution s, justification const & j, bo
         });
 }
 
-constraints metavar_closure::mk_constraints(substitution s, justification const & j, bool relax) const {
+constraints metavar_closure::mk_constraints(substitution s, justification const & j) const {
     buffer<constraint> cs;
-    mk_constraints(s, j, relax, cs);
+    mk_constraints(s, j, cs);
     return to_list(cs.begin(), cs.end());
 }
 }
diff --git a/src/library/metavar_closure.h b/src/library/metavar_closure.h
index 4c86fea04..41a998a37 100644
--- a/src/library/metavar_closure.h
+++ b/src/library/metavar_closure.h
@@ -30,10 +30,10 @@ class metavar_closure {
     void for_each_expr_mvar(std::function<void(expr const &)> const & fn) const;
     void for_each_level_mvar(std::function<void(level const &)> const & fn) const;
     /** \brief For each collected metavariable ?m, store in \c r constraints of the form ?m =?= s(?m)
-        if ?m is assigned by \c s. The constraints are justified by \c j and \c relax
+        if ?m is assigned by \c s. The constraints are justified by \c j
         \see mk_eq_cnstr
     */
-    void mk_constraints(substitution s, justification const & j, bool relax, buffer<constraint> & r) const;
-    constraints mk_constraints(substitution s, justification const & j, bool relax) const;
+    void mk_constraints(substitution s, justification const & j, buffer<constraint> & r) const;
+    constraints mk_constraints(substitution s, justification const & j) const;
 };
 }
diff --git a/src/library/module.cpp b/src/library/module.cpp
index 4ab83ba1d..9fd917c56 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -232,7 +232,7 @@ environment declare_quotient(environment const & env) {
     return add(new_env, *g_quotient, [=](serializer &) {});
 }
 
-static void quotient_reader(deserializer &, module_idx, shared_environment & senv,
+static void quotient_reader(deserializer &, shared_environment & senv,
                             std::function<void(asynch_update_fn const &)>  &,
                             std::function<void(delayed_update_fn const &)> &) {
     senv.update([&](environment const & env) {
@@ -245,7 +245,7 @@ environment declare_hits(environment const & env) {
     return add(new_env, *g_hits, [=](serializer &) {});
 }
 
-static void hits_reader(deserializer &, module_idx, shared_environment & senv,
+static void hits_reader(deserializer &, shared_environment & senv,
                         std::function<void(asynch_update_fn const &)>  &,
                         std::function<void(delayed_update_fn const &)> &) {
     senv.update([&](environment const & env) {
@@ -266,7 +266,7 @@ environment add_inductive(environment                  env,
         });
 }
 
-static void inductive_reader(deserializer & d, module_idx, shared_environment & senv,
+static void inductive_reader(deserializer & d, shared_environment & senv,
                              std::function<void(asynch_update_fn const &)>  &,
                              std::function<void(delayed_update_fn const &)> &) {
     inductive_decls ds = read_inductive_decls(d);
@@ -282,7 +282,7 @@ environment add_inductive(environment const & env, name const & ind_name, level_
 } // end of namespace module
 
 struct import_modules_fn {
-    typedef std::tuple<module_idx, unsigned, delayed_update_fn> delayed_update;
+    typedef std::tuple<unsigned, unsigned, delayed_update_fn> delayed_update;
     shared_environment             m_senv;
     unsigned                       m_num_threads;
     bool                           m_keep_proofs;
@@ -367,7 +367,7 @@ struct import_modules_fn {
             module_info_ptr r = std::make_shared<module_info>();
             r->m_fname        = fname;
             r->m_counter      = 0;
-            r->m_module_idx   = g_null_module_idx;
+            r->m_module_idx   = 0;
             m_import_counter++;
             std::string new_base = dirname(fname.c_str());
             std::swap(r->m_obj_code, code);
@@ -407,9 +407,9 @@ struct import_modules_fn {
         return mk_axiom(decl.get_name(), decl.get_univ_params(), decl.get_type());
     }
 
-    void import_decl(deserializer & d, module_idx midx) {
-        declaration decl = read_declaration(d, midx);
-        lean_assert(!decl.is_definition() || decl.get_module_idx() == midx);
+    void import_decl(deserializer & d) {
+        declaration decl = read_declaration(d);
+        lean_assert(!decl.is_definition());
         environment env  = m_senv.env();
         decl = unfold_untrusted_macros(env, decl);
         if (decl.get_name() == get_sorry_name() && has_sorry(env))
@@ -465,7 +465,7 @@ struct import_modules_fn {
             if (k == g_olean_end_file) {
                 break;
             } else if (k == *g_decl_key) {
-                import_decl(d, r->m_module_idx);
+                import_decl(d);
             } else if (k == *g_glvl_key) {
                 import_universe(d);
             } else {
@@ -473,7 +473,7 @@ struct import_modules_fn {
                 auto it = readers.find(k);
                 if (it == readers.end())
                     throw exception(sstream() << "file '" << r->m_fname << "' has been corrupted, unknown object");
-                it->second(d, r->m_module_idx, m_senv, add_asynch_update, add_delayed_update);
+                it->second(d, m_senv, add_asynch_update, add_delayed_update);
             }
             obj_counter++;
         }
diff --git a/src/library/module.h b/src/library/module.h
index 9c36f7342..79ffb8c6a 100644
--- a/src/library/module.h
+++ b/src/library/module.h
@@ -76,7 +76,7 @@ typedef std::function<environment(environment const & env, io_state const & ios)
      2- Asynchronous update using add_asynch_update.
      3- Delayed update using add_delayed_update.
 */
-typedef void (*module_object_reader)(deserializer & d, module_idx midx, shared_environment & senv,
+typedef void (*module_object_reader)(deserializer & d, shared_environment & senv,
                                      std::function<void(asynch_update_fn const &)> & add_asynch_update,
                                      std::function<void(delayed_update_fn const &)> & add_delayed_update);
 
diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index 0ce38bedb..5927d6af6 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -334,13 +334,13 @@ public:
 };
 
 expr normalize(environment const & env, expr const & e, bool eta) {
-    auto tc          = mk_type_checker(env, true);
+    auto tc          = mk_type_checker(env);
     bool save_cnstrs = false;
     return normalize_fn(*tc, save_cnstrs, eta)(e);
 }
 
 expr normalize(environment const & env, level_param_names const & ls, expr const & e, bool eta) {
-    auto tc          = mk_type_checker(env, true);
+    auto tc          = mk_type_checker(env);
     bool save_cnstrs = false;
     return normalize_fn(*tc, save_cnstrs, eta)(ls, e);
 }
diff --git a/src/library/private.cpp b/src/library/private.cpp
index 65ce0564c..6aaa0ce2f 100644
--- a/src/library/private.cpp
+++ b/src/library/private.cpp
@@ -53,7 +53,7 @@ pair<environment, name> add_private_name(environment const & env, name const & n
     return mk_pair(new_env, r);
 }
 
-static void private_reader(deserializer & d, module_idx, shared_environment & senv,
+static void private_reader(deserializer & d, shared_environment & senv,
                            std::function<void(asynch_update_fn const &)> &,
                            std::function<void(delayed_update_fn const &)> &) {
     name n, h;
diff --git a/src/library/projection.cpp b/src/library/projection.cpp
index c615b826c..7fcb14e2f 100644
--- a/src/library/projection.cpp
+++ b/src/library/projection.cpp
@@ -56,7 +56,7 @@ projection_info const * get_projection_info(environment const & env, name const
     return ext.m_info.find(p);
 }
 
-static void projection_info_reader(deserializer & d, module_idx, shared_environment & senv,
+static void projection_info_reader(deserializer & d, shared_environment & senv,
                                    std::function<void(asynch_update_fn const &)> &,
                                    std::function<void(delayed_update_fn const &)> &) {
     name p, mk; unsigned nparams, i; bool inst_implicit;
diff --git a/src/library/protected.cpp b/src/library/protected.cpp
index 26b162b8b..fcb125794 100644
--- a/src/library/protected.cpp
+++ b/src/library/protected.cpp
@@ -37,7 +37,7 @@ environment add_protected(environment const & env, name const & n) {
     return module::add(new_env, *g_prt_key, [=](serializer & s) { s << n; });
 }
 
-static void protected_reader(deserializer & d, module_idx, shared_environment & senv,
+static void protected_reader(deserializer & d, shared_environment & senv,
                              std::function<void(asynch_update_fn const &)> &,
                              std::function<void(delayed_update_fn const &)> &) {
     name n;
diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp
index cde5e4aa7..db4980780 100644
--- a/src/library/reducible.cpp
+++ b/src/library/reducible.cpp
@@ -86,7 +86,7 @@ static void check_declaration(environment const & env, name const & n) {
         throw exception(sstream() << "invalid reducible command, '" << n << "' is not a definition");
     if (d.is_theorem())
         throw exception(sstream() << "invalid reducible command, '" << n << "' is a theorem");
-    if (d.is_opaque() && d.get_module_idx() != g_main_module_idx)
+    if (d.is_opaque())
         throw exception(sstream() << "invalid reducible command, '" << n << "' is an opaque definition");
 }
 
@@ -105,8 +105,8 @@ bool is_at_least_quasireducible(environment const & env, name const & n) {
     return r == reducible_status::Reducible || r == reducible_status::Quasireducible;
 }
 
-unfold_reducible_converter::unfold_reducible_converter(environment const & env, bool relax_main_opaque, bool memoize):
-    default_converter(env, relax_main_opaque, memoize) {
+unfold_reducible_converter::unfold_reducible_converter(environment const & env, bool memoize):
+    default_converter(env, memoize) {
     m_state = reducible_ext::get_state(env);
 }
 
@@ -116,8 +116,8 @@ bool unfold_reducible_converter::is_opaque(declaration const & d) const {
     return default_converter::is_opaque(d);
 }
 
-unfold_quasireducible_converter::unfold_quasireducible_converter(environment const & env, bool relax_main_opaque, bool memoize):
-    default_converter(env, relax_main_opaque, memoize) {
+unfold_quasireducible_converter::unfold_quasireducible_converter(environment const & env, bool memoize):
+    default_converter(env, memoize) {
     m_state = reducible_ext::get_state(env);
 }
 
@@ -127,8 +127,8 @@ bool unfold_quasireducible_converter::is_opaque(declaration const & d) const {
     return default_converter::is_opaque(d);
 }
 
-unfold_semireducible_converter::unfold_semireducible_converter(environment const & env, bool relax_main_opaque, bool memoize):
-    default_converter(env, relax_main_opaque, memoize) {
+unfold_semireducible_converter::unfold_semireducible_converter(environment const & env, bool memoize):
+    default_converter(env, memoize) {
     m_state = reducible_ext::get_state(env);
 }
 
@@ -139,29 +139,28 @@ bool unfold_semireducible_converter::is_opaque(declaration const & d) const {
 }
 
 std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator const & ngen,
-                                              bool relax_main_opaque, reducible_behavior rb,
-                                              bool memoize) {
+                                              reducible_behavior rb, bool memoize) {
     switch (rb) {
     case UnfoldReducible:
         return std::unique_ptr<type_checker>(new type_checker(env, ngen,
-               std::unique_ptr<converter>(new unfold_reducible_converter(env, relax_main_opaque, memoize))));
+               std::unique_ptr<converter>(new unfold_reducible_converter(env, memoize))));
     case UnfoldQuasireducible:
         return std::unique_ptr<type_checker>(new type_checker(env, ngen,
-               std::unique_ptr<converter>(new unfold_quasireducible_converter(env, relax_main_opaque, memoize))));
+               std::unique_ptr<converter>(new unfold_quasireducible_converter(env, memoize))));
     case UnfoldSemireducible:
         return std::unique_ptr<type_checker>(new type_checker(env, ngen,
-               std::unique_ptr<converter>(new unfold_semireducible_converter(env, relax_main_opaque, memoize))));
+               std::unique_ptr<converter>(new unfold_semireducible_converter(env, memoize))));
     }
     lean_unreachable();
 }
 
-std::unique_ptr<type_checker> mk_type_checker(environment const & env, bool relax_main_opaque, reducible_behavior rb) {
-    return mk_type_checker(env, name_generator(*g_tmp_prefix), relax_main_opaque, rb);
+std::unique_ptr<type_checker> mk_type_checker(environment const & env, reducible_behavior rb) {
+    return mk_type_checker(env, name_generator(*g_tmp_prefix), rb);
 }
 
 class opaque_converter : public default_converter {
 public:
-    opaque_converter(environment const & env): default_converter(env, true, true) {}
+    opaque_converter(environment const & env): default_converter(env) {}
     virtual bool is_opaque(declaration const &) const { return true; }
 };
 
@@ -187,13 +186,13 @@ static int mk_opaque_type_checker(lua_State * L) {
 static int mk_reducible_checker_core(lua_State * L, reducible_behavior rb) {
     int nargs = lua_gettop(L);
     if (nargs == 0) {
-        type_checker_ref r(mk_type_checker(get_global_environment(L), name_generator(), false, rb));
+        type_checker_ref r(mk_type_checker(get_global_environment(L), name_generator(), rb));
         return push_type_checker_ref(L, r);
     } else if (nargs == 1) {
-        type_checker_ref r(mk_type_checker(to_environment(L, 1), name_generator(), false, rb));
+        type_checker_ref r(mk_type_checker(to_environment(L, 1), name_generator(), rb));
         return push_type_checker_ref(L, r);
     } else {
-        type_checker_ref r(mk_type_checker(to_environment(L, 1), to_name_generator(L, 2), false, rb));
+        type_checker_ref r(mk_type_checker(to_environment(L, 1), to_name_generator(L, 2), rb));
         return push_type_checker_ref(L, r);
     }
 }
diff --git a/src/library/reducible.h b/src/library/reducible.h
index 6dca29383..9c72b612b 100644
--- a/src/library/reducible.h
+++ b/src/library/reducible.h
@@ -40,7 +40,7 @@ public:
 class unfold_reducible_converter : public default_converter {
     reducible_state m_state;
 public:
-    unfold_reducible_converter(environment const & env, bool relax_main_opaque, bool memoize);
+    unfold_reducible_converter(environment const & env, bool memoize);
     virtual bool is_opaque(declaration const & d) const;
 };
 
@@ -48,7 +48,7 @@ public:
 class unfold_quasireducible_converter : public default_converter {
     reducible_state m_state;
 public:
-    unfold_quasireducible_converter(environment const & env, bool relax_main_opaque, bool memoize);
+    unfold_quasireducible_converter(environment const & env, bool memoize);
     virtual bool is_opaque(declaration const & d) const;
 };
 
@@ -56,7 +56,7 @@ public:
 class unfold_semireducible_converter : public default_converter {
     reducible_state m_state;
 public:
-    unfold_semireducible_converter(environment const & env, bool relax_main_opaque, bool memoize);
+    unfold_semireducible_converter(environment const & env, bool memoize);
     virtual bool is_opaque(declaration const & d) const;
 };
 
@@ -64,10 +64,9 @@ enum reducible_behavior { UnfoldReducible, UnfoldQuasireducible, UnfoldSemireduc
 
 /** \brief Create a type checker that takes the "reducibility" hints into account. */
 std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator const & ngen,
-                                              bool relax_main_opaque = true, reducible_behavior r = UnfoldSemireducible,
+                                              reducible_behavior r = UnfoldSemireducible,
                                               bool memoize = true);
-std::unique_ptr<type_checker> mk_type_checker(environment const & env, bool relax_main_opaque,
-                                              reducible_behavior r = UnfoldSemireducible);
+std::unique_ptr<type_checker> mk_type_checker(environment const & env, reducible_behavior r = UnfoldSemireducible);
 
 /** \brief Create a type checker that treats all definitions as opaque. */
 std::unique_ptr<type_checker> mk_opaque_type_checker(environment const & env, name_generator const & ngen);
diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp
index 975a7f88c..a622dbe8c 100644
--- a/src/library/scoped_ext.cpp
+++ b/src/library/scoped_ext.cpp
@@ -159,7 +159,7 @@ environment push_scope(environment const & env, io_state const & ios, scope_kind
     return r;
 }
 
-static void namespace_reader(deserializer & d, module_idx, shared_environment &,
+static void namespace_reader(deserializer & d, shared_environment &,
                              std::function<void(asynch_update_fn const &)> &,
                              std::function<void(delayed_update_fn const &)> & add_delayed_update) {
     name n;
diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h
index 76f07c22c..a755b1ce1 100644
--- a/src/library/scoped_ext.h
+++ b/src/library/scoped_ext.h
@@ -244,7 +244,7 @@ public:
             return update(env, get(env)._add_entry(env, ios, e));
         }
     }
-    static void reader(deserializer & d, module_idx, shared_environment &,
+    static void reader(deserializer & d, shared_environment &,
                        std::function<void(asynch_update_fn const &)> &,
                        std::function<void(delayed_update_fn const &)> & add_delayed_update) {
         name n;
diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index db749151d..38a685590 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -80,8 +80,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
     }
     bool class_inst   = get_apply_class_instance(ios.get_options());
     name_generator ngen = s.get_ngen();
-    bool relax_opaque = s.relax_main_opaque();
-    std::shared_ptr<type_checker> tc(mk_type_checker(env, ngen.mk_child(), relax_opaque));
+    std::shared_ptr<type_checker> tc(mk_type_checker(env, ngen.mk_child()));
     goal  g           = head(gs);
     goals tail_gs     = tail(gs);
     expr  t           = g.get_type();
@@ -120,7 +119,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
                 bool is_strict       = false;
                 auto mc = mk_class_instance_elaborator(
                     env, ios, ctx, ngen.next(), optional<name>(),
-                    relax_opaque, use_local_insts, is_strict,
+                    use_local_insts, is_strict,
                     some_expr(binding_domain(e_t)), e.get_tag(), cfg, nullptr);
                 meta    = mc.first;
                 cs.push_back(mc.second);
@@ -133,7 +132,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
         }
     }
     metavar_closure cls(t);
-    cls.mk_constraints(s.get_subst(), justification(), relax_opaque);
+    cls.mk_constraints(s.get_subst(), justification());
     pair<bool, constraint_seq> dcs = tc->is_def_eq(t, e_t);
     if (!dcs.first) {
         throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) {
diff --git a/src/library/tactic/check_expr_tactic.cpp b/src/library/tactic/check_expr_tactic.cpp
index d2fc96c30..374726bc1 100644
--- a/src/library/tactic/check_expr_tactic.cpp
+++ b/src/library/tactic/check_expr_tactic.cpp
@@ -22,7 +22,7 @@ tactic check_expr_tactic(elaborate_fn const & elab, expr const & e,
             goal const & g      = head(gs);
             name_generator ngen = s.get_ngen();
             expr new_e = std::get<0>(elab(g, ngen.mk_child(), e, none_expr(), s.get_subst(), false));
-            auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
+            auto tc = mk_type_checker(env, ngen.mk_child());
             expr new_t = tc->infer(new_e).first;
             auto out = regular(env, ios);
             flycheck_information info(out);
diff --git a/src/library/tactic/class_instance_synth.cpp b/src/library/tactic/class_instance_synth.cpp
index ea46c6389..2c651d83b 100644
--- a/src/library/tactic/class_instance_synth.cpp
+++ b/src/library/tactic/class_instance_synth.cpp
@@ -99,7 +99,6 @@ struct class_instance_context {
     name_generator            m_ngen;
     type_checker_ptr          m_tc;
     expr                      m_main_meta;
-    bool                      m_relax;
     bool                      m_use_local_instances;
     bool                      m_trace_instances;
     bool                      m_conservative;
@@ -107,19 +106,18 @@ struct class_instance_context {
     char const *              m_fname;
     optional<pos_info>        m_pos;
     class_instance_context(environment const & env, io_state const & ios,
-                           name const & prefix, bool relax, bool use_local_instances):
+                           name const & prefix, bool use_local_instances):
         m_ios(ios),
         m_ngen(prefix),
-        m_relax(relax),
         m_use_local_instances(use_local_instances) {
         m_fname           = nullptr;
         m_trace_instances = get_class_trace_instances(ios.get_options());
         m_max_depth       = get_class_instance_max_depth(ios.get_options());
         m_conservative    = get_class_conservative(ios.get_options());
         if (m_conservative)
-            m_tc = mk_type_checker(env, m_ngen.mk_child(), false, UnfoldReducible);
+            m_tc = mk_type_checker(env, m_ngen.mk_child(), UnfoldReducible);
         else
-            m_tc = mk_type_checker(env, m_ngen.mk_child(), m_relax);
+            m_tc = mk_type_checker(env, m_ngen.mk_child());
         options opts      = m_ios.get_options();
         opts              = opts.update_if_undef(get_pp_purify_metavars_name(), false);
         opts              = opts.update_if_undef(get_pp_implicit_name(), true);
@@ -250,8 +248,7 @@ struct class_instance_elaborator : public choice_iterator {
             }
             r = Fun(locals, r);
             trace(meta_type, r);
-            bool relax   = m_C->m_relax;
-            constraint c = mk_eq_cnstr(m_meta, r, m_jst, relax);
+            constraint c = mk_eq_cnstr(m_meta, r, m_jst);
             return optional<constraints>(mk_constraints(c, cs));
         } catch (exception &) {
             return optional<constraints>();
@@ -315,9 +312,7 @@ constraint mk_class_instance_cnstr(std::shared_ptr<class_instance_context> const
         }
     };
     bool owner      = false;
-    bool relax      = C->m_relax;
-    return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Basic),
-                           owner, j, relax);
+    return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Basic), owner, j);
 }
 
 pair<expr, constraint> mk_class_instance_elaborator(std::shared_ptr<class_instance_context> const & C, local_context const & ctx,
@@ -362,8 +357,7 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
                                          });
             metavar_closure cls(new_meta);
             cls.add(meta_type);
-            bool relax     = C->m_relax;
-            constraints cs = cls.mk_constraints(new_s, new_j, relax);
+            constraints cs = cls.mk_constraints(new_s, new_j);
             return append(cs, postponed);
         };
 
@@ -430,8 +424,7 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
         }
     };
     bool owner = false;
-    bool relax = C->m_relax;
-    return mk_choice_cnstr(m, choice_fn, factor, owner, j, relax);
+    return mk_choice_cnstr(m, choice_fn, factor, owner, j);
 }
 
 /** \brief Create a metavariable, and attach choice constraint for generating
@@ -439,10 +432,10 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
 */
 pair<expr, constraint> mk_class_instance_elaborator(
     environment const & env, io_state const & ios, local_context const & ctx,
-    name const & prefix, optional<name> const & suffix, bool relax, bool use_local_instances,
+    name const & prefix, optional<name> const & suffix, bool use_local_instances,
     bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg,
     pos_info_provider const * pip) {
-    auto C       = std::make_shared<class_instance_context>(env, ios, prefix, relax, use_local_instances);
+    auto C       = std::make_shared<class_instance_context>(env, ios, prefix, use_local_instances);
     expr m       = ctx.mk_meta(C->m_ngen, suffix, type, g);
     C->set_main_meta(m);
     if (pip)
@@ -452,9 +445,9 @@ pair<expr, constraint> mk_class_instance_elaborator(
 }
 
 optional<expr> mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx,
-                                 name const & prefix, expr const & type, bool relax_opaque, bool use_local_instances,
+                                 name const & prefix, expr const & type, bool use_local_instances,
                                  unifier_config const & cfg) {
-    auto C = std::make_shared<class_instance_context>(env, ios, prefix, relax_opaque, use_local_instances);
+    auto C = std::make_shared<class_instance_context>(env, ios, prefix, use_local_instances);
     if (!is_ext_class(C->tc(), type))
         return none_expr();
     expr meta       = ctx.mk_meta(C->m_ngen, some_expr(type), type.get_tag());
@@ -482,10 +475,10 @@ optional<expr> mk_class_instance(environment const & env, io_state const & ios,
 }
 
 optional<expr> mk_class_instance(environment const & env, io_state const & ios, list<expr> const & ctx,
-                                 name const & prefix, expr const & type, bool relax_opaque, bool use_local_instances,
+                                 name const & prefix, expr const & type, bool use_local_instances,
                                  unifier_config const & cfg) {
     local_context lctx(ctx);
-    return mk_class_instance(env, ios, lctx, prefix, type, relax_opaque, use_local_instances, cfg);
+    return mk_class_instance(env, ios, lctx, prefix, type, use_local_instances, cfg);
 }
 
 optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type) {
diff --git a/src/library/tactic/class_instance_synth.h b/src/library/tactic/class_instance_synth.h
index deb282445..ff3c70a7a 100644
--- a/src/library/tactic/class_instance_synth.h
+++ b/src/library/tactic/class_instance_synth.h
@@ -19,8 +19,6 @@ class type_checker;
     \param ctx Local context where placeholder is located
     \param prefix Prefix for metavariables that will be created by this procedure
     \param suffix If provided, then it is added to the main metavariable created by this procedure.
-    \param relax True if opaque constants in the current module should be treated
-                 as transparent
     \param use_local_instances If instances in the local context should be used
                                in the class-instance resolution
     \param is_strict True if constraint should fail if not solution is found,
@@ -30,17 +28,17 @@ class type_checker;
 */
 pair<expr, constraint> mk_class_instance_elaborator(
     environment const & env, io_state const & ios, local_context const & ctx,
-    name const & prefix, optional<name> const & suffix, bool relax_opaque, bool use_local_instances,
+    name const & prefix, optional<name> const & suffix, bool use_local_instances,
     bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg,
     pos_info_provider const * pip);
 
 /** \brief Create/synthesize a term of the class instance \c type. */
 optional<expr> mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx,
-                                 name const & prefix, expr const & type, bool relax_opaque = true, bool use_local_instances = true,
+                                 name const & prefix, expr const & type, bool use_local_instances = true,
                                  unifier_config const & cfg = unifier_config());
 
 optional<expr> mk_class_instance(environment const & env, io_state const & ios, list<expr> const & ctx,
-                                 name const & prefix, expr const & type, bool relax_opaque = true, bool use_local_instances = true,
+                                 name const & prefix, expr const & type, bool use_local_instances = true,
                                  unifier_config const & cfg = unifier_config());
 
 /** \breif Try to synthesize an inhabitant for (is_hset type) using class instance resolution */
diff --git a/src/library/tactic/congruence_tactic.cpp b/src/library/tactic/congruence_tactic.cpp
index ee262cb53..87eb4bd00 100644
--- a/src/library/tactic/congruence_tactic.cpp
+++ b/src/library/tactic/congruence_tactic.cpp
@@ -23,7 +23,7 @@ tactic congruence_tactic() {
         expr t              = g.get_type();
         substitution subst  = s.get_subst();
         name_generator ngen = s.get_ngen();
-        auto tc             = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
+        auto tc             = mk_type_checker(env, ngen.mk_child());
         constraint_seq cs;
         t = tc->whnf(t, cs);
         expr lhs, rhs;
diff --git a/src/library/tactic/constructor_tactic.cpp b/src/library/tactic/constructor_tactic.cpp
index c1907477d..114cfaa25 100644
--- a/src/library/tactic/constructor_tactic.cpp
+++ b/src/library/tactic/constructor_tactic.cpp
@@ -31,7 +31,7 @@ tactic constructor_tactic(elaborate_fn const & elab, optional<unsigned> _i, opti
         }
         constraint_seq cs;
         name_generator ngen = s.get_ngen();
-        auto tc             = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
+        auto tc             = mk_type_checker(env, ngen.mk_child());
         goal const & g      = head(gs);
         expr t              = tc->whnf(g.get_type(), cs);
         buffer<expr> I_args;
diff --git a/src/library/tactic/contradiction_tactic.cpp b/src/library/tactic/contradiction_tactic.cpp
index 9c298df14..c6c7d597e 100644
--- a/src/library/tactic/contradiction_tactic.cpp
+++ b/src/library/tactic/contradiction_tactic.cpp
@@ -24,7 +24,7 @@ tactic contradiction_tactic() {
         expr const & t      = g.get_type();
         substitution subst  = s.get_subst();
         name_generator ngen = s.get_ngen();
-        auto tc             = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
+        auto tc             = mk_type_checker(env, ngen.mk_child());
         buffer<expr> hyps;
         g.get_hyps(hyps);
         for (expr const & h : hyps) {
diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp
index 01818fa04..178b710cc 100644
--- a/src/library/tactic/exact_tactic.cpp
+++ b/src/library/tactic/exact_tactic.cpp
@@ -62,7 +62,7 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type
                     if (allow_metavars) {
                         buffer<goal> new_goals;
                         name_generator ngen = new_s.get_ngen();
-                        auto tc             = mk_type_checker(env, ngen.mk_child(), new_s.relax_main_opaque());
+                        auto tc             = mk_type_checker(env, ngen.mk_child());
                         for_each(*new_e, [&](expr const & m, unsigned) {
                                 if (!has_expr_metavar(m))
                                     return false;
diff --git a/src/library/tactic/exfalso_tactic.cpp b/src/library/tactic/exfalso_tactic.cpp
index 7d76c9bb4..f192183f2 100644
--- a/src/library/tactic/exfalso_tactic.cpp
+++ b/src/library/tactic/exfalso_tactic.cpp
@@ -24,7 +24,7 @@ tactic exfalso_tactic() {
         expr const & t      = g.get_type();
         substitution subst  = s.get_subst();
         name_generator ngen = s.get_ngen();
-        auto tc             = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
+        auto tc             = mk_type_checker(env, ngen.mk_child());
         expr false_expr     = mk_false(env);
         expr new_meta       = g.mk_meta(ngen.next(), false_expr);
         goal new_goal(new_meta, false_expr);
diff --git a/src/library/tactic/injection_tactic.cpp b/src/library/tactic/injection_tactic.cpp
index 73919c54e..763040003 100644
--- a/src/library/tactic/injection_tactic.cpp
+++ b/src/library/tactic/injection_tactic.cpp
@@ -50,7 +50,7 @@ tactic intros_num_tactic(unsigned num, list<name> _ns) {
             return proof_state_seq();
         goal const & g      = head(gs);
         name_generator ngen = s.get_ngen();
-        auto tc             = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
+        auto tc             = mk_type_checker(env, ngen.mk_child());
         expr t              = g.get_type();
         expr m              = g.get_meta();
 
@@ -150,7 +150,7 @@ tactic injection_tactic_core(expr const & e, unsigned num, list<name> const & id
         expr t                 = head(gs).get_type();
         constraint_seq cs;
         name_generator ngen = s.get_ngen();
-        auto tc             = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
+        auto tc             = mk_type_checker(env, ngen.mk_child());
         expr e_type         = tc->whnf(tc->infer(e, cs), cs);
         expr lhs, rhs;
         if (!is_eq(e_type, lhs, rhs)) {
diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/tactic/intros_tactic.cpp
index d09c97fef..132bfcf95 100644
--- a/src/library/tactic/intros_tactic.cpp
+++ b/src/library/tactic/intros_tactic.cpp
@@ -21,7 +21,7 @@ tactic intros_tactic(list<name> _ns) {
         }
         goal const & g      = head(gs);
         name_generator ngen = s.get_ngen();
-        auto tc             = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
+        auto tc             = mk_type_checker(env, ngen.mk_child());
         expr t              = g.get_type();
         expr m              = g.get_meta();
         bool gen_names      = empty(ns);
diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp
index 04076c169..515bfc2ec 100644
--- a/src/library/tactic/inversion_tactic.cpp
+++ b/src/library/tactic/inversion_tactic.cpp
@@ -1096,7 +1096,7 @@ tactic inversion_tactic(name const & n, list<name> const & ids) {
         goal  g           = head(gs);
         goals tail_gs     = tail(gs);
         name_generator ngen              = ps.get_ngen();
-        std::unique_ptr<type_checker> tc = mk_type_checker(env, ngen.mk_child(), ps.relax_main_opaque());
+        std::unique_ptr<type_checker> tc = mk_type_checker(env, ngen.mk_child());
         inversion_tac tac(env, ios, ngen, *tc, ps.get_subst(), ids, ps.report_failure());
         if (auto res = tac.execute(g, n, implementation_list())) {
             proof_state new_s(ps, append(res->m_goals, tail_gs), res->m_subst, res->m_ngen);
diff --git a/src/library/tactic/let_tactic.cpp b/src/library/tactic/let_tactic.cpp
index 14b1e51c7..b7e24a24e 100644
--- a/src/library/tactic/let_tactic.cpp
+++ b/src/library/tactic/let_tactic.cpp
@@ -34,7 +34,7 @@ tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
             std::tie(new_e, new_subst, cs) = esc;
             if (cs)
                 throw_tactic_exception_if_enabled(s, "invalid 'let' tactic, fail to resolve generated constraints");
-            auto tc         = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
+            auto tc         = mk_type_checker(env, ngen.mk_child());
             expr new_e_type = tc->infer(new_e).first;
             expr new_local  = mk_local(ngen.next(), id, new_e_type, binder_info());
             buffer<expr> hyps;
diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp
index 203a145bd..b0663999b 100644
--- a/src/library/tactic/proof_state.cpp
+++ b/src/library/tactic/proof_state.cpp
@@ -31,8 +31,8 @@ bool get_proof_state_goal_names(options const & opts) {
 }
 
 proof_state::proof_state(goals const & gs, substitution const & s, name_generator const & ngen,
-                         constraints const & postponed, bool relax_main_opaque, bool report_failure):
-    m_goals(gs), m_subst(s), m_ngen(ngen), m_postponed(postponed), m_relax_main_opaque(relax_main_opaque),
+                         constraints const & postponed, bool report_failure):
+    m_goals(gs), m_subst(s), m_ngen(ngen), m_postponed(postponed),
     m_report_failure(report_failure) {
     if (std::any_of(gs.begin(), gs.end(),
                     [&](goal const & g) { return s.is_assigned(g.get_mvar()); })) {
@@ -81,13 +81,12 @@ goals map_goals(proof_state const & s, std::function<optional<goal>(goal const &
         });
 }
 
-proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen,
-                           bool relax_main_opaque) {
-    return proof_state(goals(goal(meta, type)), subst, ngen, constraints(), relax_main_opaque);
+proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen) {
+    return proof_state(goals(goal(meta, type)), subst, ngen, constraints());
 }
 
-proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen, bool relax_main_opaque) {
-    return to_proof_state(meta, type, substitution(), ngen, relax_main_opaque);
+proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen) {
+    return to_proof_state(meta, type, substitution(), ngen);
 }
 
 proof_state apply_substitution(proof_state const & s) {
@@ -180,9 +179,8 @@ static int mk_proof_state(lua_State * L) {
     } else if (nargs == 3 && is_proof_state(L, 1)) {
         return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_substitution(L, 3)));
     } else if (nargs == 3) {
-        bool relax_main_opaque = true;
         return push_proof_state(L, proof_state(to_goals(L, 1), to_substitution(L, 2), to_name_generator(L, 3),
-                                               constraints(), relax_main_opaque));
+                                               constraints()));
     } else {
         throw exception("proof_state invalid number of arguments");
     }
@@ -191,11 +189,10 @@ static int mk_proof_state(lua_State * L) {
 static name * g_tmp_prefix = nullptr;
 static int to_proof_state(lua_State * L) {
     int nargs = lua_gettop(L);
-    bool relax_main_opaque = true;
     if (nargs == 2)
-        return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), name_generator(*g_tmp_prefix), relax_main_opaque));
+        return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), name_generator(*g_tmp_prefix)));
     else
-        return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), to_name_generator(L, 3), relax_main_opaque));
+        return push_proof_state(L, to_proof_state(to_expr(L, 1), to_expr(L, 2), to_name_generator(L, 3)));
 }
 
 static int proof_state_tostring(lua_State * L) {
diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h
index 8b3f15ff5..6f11d8bfa 100644
--- a/src/library/tactic/proof_state.h
+++ b/src/library/tactic/proof_state.h
@@ -21,19 +21,18 @@ class proof_state {
     substitution     m_subst;
     name_generator   m_ngen;
     constraints      m_postponed;
-    bool             m_relax_main_opaque;
     bool             m_report_failure;
 
     format pp_core(std::function<formatter()> const & mk_fmt, options const & opts) const;
 
 public:
     proof_state(goals const & gs, substitution const & s, name_generator const & ngen, constraints const & postponed,
-                bool relax_main_opaque, bool report_failure = true);
+                bool report_failure = true);
     proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen,
                 constraints const & postponed):
-        proof_state(gs, subst, ngen, postponed, s.relax_main_opaque(), s.report_failure()) {}
+        proof_state(gs, subst, ngen, postponed, s.report_failure()) {}
     proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen):
-        proof_state(gs, subst, ngen, s.m_postponed, s.relax_main_opaque(), s.report_failure()) {}
+        proof_state(gs, subst, ngen, s.m_postponed, s.report_failure()) {}
     proof_state(proof_state const & s, goals const & gs, substitution const & subst):
         proof_state(s, gs, subst, s.m_ngen) {}
     proof_state(proof_state const & s, goals const & gs, name_generator const & ngen):
@@ -42,7 +41,7 @@ public:
         proof_state(s, gs, s.m_subst) {}
     proof_state(proof_state const & s, substitution const & subst, name_generator const & ngen,
                 constraints const & postponed):
-        proof_state(s.m_goals, subst, ngen, postponed, s.relax_main_opaque(), s.report_failure()) {}
+        proof_state(s.m_goals, subst, ngen, postponed, s.report_failure()) {}
     proof_state(proof_state const & s, name_generator const & ngen, constraints const & postponed):
         proof_state(s, s.m_goals, s.m_subst, ngen, postponed) {}
     proof_state(proof_state const & s, substitution const & subst, name_generator const & ngen):
@@ -53,14 +52,13 @@ public:
         proof_state(s, subst, s.m_ngen) {}
 
     proof_state update_report_failure(bool f) const {
-        return m_report_failure == f ? *this : proof_state(m_goals, m_subst, m_ngen, m_postponed, m_relax_main_opaque, f);
+        return m_report_failure == f ? *this : proof_state(m_goals, m_subst, m_ngen, m_postponed, f);
     }
 
     goals const & get_goals() const { return m_goals; }
     substitution const & get_subst() const { return m_subst; }
     name_generator const & get_ngen() const { return m_ngen; }
     constraints const & get_postponed() const { return m_postponed; }
-    bool relax_main_opaque() const { return m_relax_main_opaque; }
     bool report_failure() const { return m_report_failure; }
 
     /** \brief Return true iff this state does not have any goals left */
@@ -81,9 +79,8 @@ proof_state apply_substitution(proof_state const & s);
 inline optional<proof_state> some_proof_state(proof_state const & s) { return some(s); }
 inline optional<proof_state> none_proof_state() { return optional<proof_state> (); }
 
-proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen,
-                           bool relax_main_opaque);
-proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen, bool relax_main_opaque);
+proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen);
+proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen);
 
 goals map_goals(proof_state const & s, std::function<optional<goal>(goal const & g)> f);
 
diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 66e69d0e2..fd75c40b8 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -580,9 +580,8 @@ class rewrite_fn {
         list<name> const & m_to_unfold;
         bool             & m_unfolded;
     public:
-        rewriter_converter(environment const & env, bool relax_main_opaque, list<name> const & to_unfold,
-                           bool & unfolded):
-            default_converter(env, relax_main_opaque),
+        rewriter_converter(environment const & env, list<name> const & to_unfold, bool & unfolded):
+            default_converter(env),
             m_to_unfold(to_unfold), m_unfolded(unfolded) {}
         virtual bool is_opaque(declaration const & d) const {
             if (std::find(m_to_unfold.begin(), m_to_unfold.end(), d.get_name()) != m_to_unfold.end()) {
@@ -596,9 +595,8 @@ class rewrite_fn {
 
     optional<expr> reduce(expr const & e, list<name> const & to_unfold) {
         bool unfolded          = !to_unfold;
-        bool relax_main_opaque = false;
         auto tc = new type_checker(m_env, m_ngen.mk_child(),
-                                   std::unique_ptr<converter>(new rewriter_converter(m_env, relax_main_opaque, to_unfold, unfolded)));
+                                   std::unique_ptr<converter>(new rewriter_converter(m_env, to_unfold, unfolded)));
         constraint_seq cs;
         bool use_eta = true;
         expr r = normalize(*tc, e, cs, use_eta);
@@ -941,7 +939,7 @@ class rewrite_fn {
         bool use_local_instances = true;
         bool is_strict           = false;
         return ::lean::mk_class_instance_elaborator(m_env, m_ios, m_ctx, m_ngen.next(), optional<name>(),
-                                                    m_ps.relax_main_opaque(), use_local_instances, is_strict,
+                                                    use_local_instances, is_strict,
                                                     some_expr(type), m_expr_loc.get_tag(), cfg, nullptr);
     }
 
@@ -1409,8 +1407,8 @@ class rewrite_fn {
 
     class match_converter : public unfold_reducible_converter {
     public:
-        match_converter(environment const & env, bool relax_main_opaque):
-            unfold_reducible_converter(env, relax_main_opaque, true) {}
+        match_converter(environment const & env):
+            unfold_reducible_converter(env, true) {}
         virtual bool is_opaque(declaration const & d) const {
             if (is_projection(m_env, d.get_name()))
                 return true;
@@ -1424,7 +1422,7 @@ class rewrite_fn {
             return mk_opaque_type_checker(m_env, m_ngen.mk_child());
         } else {
             return std::unique_ptr<type_checker>(new type_checker(m_env, m_ngen.mk_child(),
-                   std::unique_ptr<converter>(new match_converter(m_env, m_ps.relax_main_opaque()))));
+                   std::unique_ptr<converter>(new match_converter(m_env))));
         }
     }
 
@@ -1476,9 +1474,9 @@ class rewrite_fn {
 public:
     rewrite_fn(environment const & env, io_state const & ios, elaborate_fn const & elab, proof_state const & ps):
         m_env(env), m_ios(ios), m_elab(elab), m_ps(ps), m_ngen(ps.get_ngen()),
-        m_tc(mk_type_checker(m_env, m_ngen.mk_child(), ps.relax_main_opaque(), UnfoldQuasireducible)),
+        m_tc(mk_type_checker(m_env, m_ngen.mk_child(), UnfoldQuasireducible)),
         m_matcher_tc(mk_matcher_tc()),
-        m_relaxed_tc(mk_type_checker(m_env, m_ngen.mk_child(), ps.relax_main_opaque())),
+        m_relaxed_tc(mk_type_checker(m_env, m_ngen.mk_child())),
         m_mplugin(m_ios, *m_matcher_tc) {
         m_ps = apply_substitution(m_ps);
         goals const & gs = m_ps.get_goals();
diff --git a/src/library/tactic/util.cpp b/src/library/tactic/util.cpp
index 86b9dcc61..16803ac40 100644
--- a/src/library/tactic/util.cpp
+++ b/src/library/tactic/util.cpp
@@ -60,8 +60,7 @@ justification mk_failed_to_synthesize_jst(environment const & env, expr const &
             substitution tmp(subst);
             expr new_m    = instantiate_meta(m, tmp);
             expr new_type = type_checker(env).infer(new_m).first;
-            bool relax_main_opaque = true; // this value doesn't really matter for pretty printing
-            proof_state ps = to_proof_state(new_m, new_type, name_generator("dontcare"), relax_main_opaque);
+            proof_state ps = to_proof_state(new_m, new_type, name_generator("dontcare"));
             return format("failed to synthesize placeholder") + line() + ps.pp(fmt);
         });
 }
diff --git a/src/library/tactic/whnf_tactic.cpp b/src/library/tactic/whnf_tactic.cpp
index d50c30693..d0c78ff8d 100644
--- a/src/library/tactic/whnf_tactic.cpp
+++ b/src/library/tactic/whnf_tactic.cpp
@@ -11,13 +11,13 @@ Author: Leonardo de Moura
 #include "library/tactic/whnf_tactic.h"
 
 namespace lean {
-tactic whnf_tactic(bool relax_main_opaque) {
+tactic whnf_tactic() {
     return tactic01([=](environment const & env, io_state const & ios, proof_state const & ps) {
             goals const & gs = ps.get_goals();
             if (empty(gs))
                 return none_proof_state();
             name_generator ngen = ps.get_ngen();
-            auto tc             = mk_type_checker(env, ngen.mk_child(), relax_main_opaque);
+            auto tc             = mk_type_checker(env, ngen.mk_child());
             goal  g             = head(gs);
             goals tail_gs       = tail(gs);
             expr  type          = g.get_type();
diff --git a/src/library/tactic/whnf_tactic.h b/src/library/tactic/whnf_tactic.h
index 263783370..0ad5c0e6a 100644
--- a/src/library/tactic/whnf_tactic.h
+++ b/src/library/tactic/whnf_tactic.h
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "library/tactic/tactic.h"
 
 namespace lean {
-tactic whnf_tactic(bool relax_main_opaque = true);
+tactic whnf_tactic();
 void initialize_whnf_tactic();
 void finalize_whnf_tactic();
 }
diff --git a/src/library/unfold_macros.cpp b/src/library/unfold_macros.cpp
index 1046f619b..0c5020504 100644
--- a/src/library/unfold_macros.cpp
+++ b/src/library/unfold_macros.cpp
@@ -143,11 +143,11 @@ declaration unfold_untrusted_macros(environment const & env, declaration const &
         expr new_t = unfold_untrusted_macros(env, d.get_type(), trust_lvl);
         if (d.is_theorem()) {
             expr new_v = unfold_untrusted_macros(env, d.get_value(), trust_lvl);
-            return mk_theorem(d.get_name(), d.get_univ_params(), new_t, new_v, d.get_module_idx());
+            return mk_theorem(d.get_name(), d.get_univ_params(), new_t, new_v);
         } else if (d.is_definition()) {
             expr new_v = unfold_untrusted_macros(env, d.get_value(), trust_lvl);
             return mk_definition(d.get_name(), d.get_univ_params(), new_t, new_v,
-                                 d.is_opaque(), d.get_weight(), d.get_module_idx(), d.use_conv_opt());
+                                 d.is_opaque(), d.get_weight(), d.use_conv_opt());
         } else if (d.is_axiom()) {
             return mk_axiom(d.get_name(), d.get_univ_params(), new_t);
         } else if (d.is_constant_assumption()) {
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 2e0d0c7bb..c1be0c315 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -329,7 +329,7 @@ struct unifier_fn {
     owned_map        m_owned_map; // mapping from metavariable name m to delay factor of the choice constraint that owns m
     expr_map         m_type_map;  // auxiliary map for storing the type of the expr in choice constraints
     unifier_plugin   m_plugin;
-    type_checker_ptr m_tc[2];
+    type_checker_ptr m_tc;
     type_checker_ptr m_flex_rigid_tc; // type checker used when solving flex rigid constraints. By default,
                                       // only the definitions from the main module are treated as transparent.
     unifier_config   m_config;
@@ -438,28 +438,24 @@ struct unifier_fn {
         m_config(cfg), m_num_steps(0) {
         switch (m_config.m_kind) {
         case unifier_kind::Cheap:
-            m_tc[0] = mk_opaque_type_checker(env, m_ngen.mk_child());
-            m_tc[1] = m_tc[0];
-            m_flex_rigid_tc = m_tc[0];
+            m_tc = mk_opaque_type_checker(env, m_ngen.mk_child());
+            m_flex_rigid_tc = m_tc;
             m_config.m_computation = false;
             break;
         case unifier_kind::VeryConservative:
-            m_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false, UnfoldReducible);
-            m_tc[1] = m_tc[0];
-            m_flex_rigid_tc = m_tc[0];
+            m_tc = mk_type_checker(env, m_ngen.mk_child(), UnfoldReducible);
+            m_flex_rigid_tc = m_tc;
             m_config.m_computation = false;
             break;
         case unifier_kind::Conservative:
-            m_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false, UnfoldQuasireducible);
-            m_tc[1] = m_tc[0];
-            m_flex_rigid_tc = m_tc[0];
+            m_tc = mk_type_checker(env, m_ngen.mk_child(), UnfoldQuasireducible);
+            m_flex_rigid_tc = m_tc;
             m_config.m_computation = false;
             break;
         case unifier_kind::Liberal:
-            m_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false);
-            m_tc[1] = mk_type_checker(env, m_ngen.mk_child(), true);
+            m_tc = mk_type_checker(env, m_ngen.mk_child());
             if (!cfg.m_computation)
-                m_flex_rigid_tc = mk_type_checker(env, m_ngen.mk_child(), false, UnfoldQuasireducible);
+                m_flex_rigid_tc = mk_type_checker(env, m_ngen.mk_child(), UnfoldQuasireducible);
             break;
         default:
             lean_unreachable();
@@ -556,12 +552,10 @@ struct unifier_fn {
     }
 
     /** \brief Check if \c t1 and \c t2 are definitionally equal, if they are not, set a conflict with justification \c j
-
-        \remark If relax is true then opaque definitions from the main module are treated as transparent.
     */
-    bool is_def_eq(expr const & t1, expr const & t2, justification const & j, bool relax) {
+    bool is_def_eq(expr const & t1, expr const & t2, justification const & j) {
         try {
-            auto dcs = m_tc[relax]->is_def_eq(t1, t2, j);
+            auto dcs = m_tc->is_def_eq(t1, t2, j);
             if (!dcs.first) {
                 // std::cout << "conflict: " << t1 << " =?= " << t2 << "\n";
                 set_conflict(j);
@@ -607,37 +601,35 @@ struct unifier_fn {
 
     /** \brief Put \c e in weak head normal form.
 
-        \remark If relax is true then opaque definitions from the main module are treated as transparent.
         \remark Constraints generated in the process are stored in \c cs.
     */
-    expr whnf(expr const & e, bool relax, constraint_seq & cs) {
-        return m_tc[relax]->whnf(e, cs);
+    expr whnf(expr const & e, constraint_seq & cs) {
+        return m_tc->whnf(e, cs);
     }
 
     /** \brief Infer \c e type.
 
         \remark Return none if an exception was throw when inferring the type.
-        \remark If relax is true then opaque definitions from the main module are treated as transparent.
         \remark Constraints generated in the process are stored in \c cs.
     */
-    optional<expr> infer(expr const & e, bool relax, constraint_seq & cs) {
+    optional<expr> infer(expr const & e, constraint_seq & cs) {
         try {
-            return some_expr(m_tc[relax]->infer(e, cs));
+            return some_expr(m_tc->infer(e, cs));
         } catch (exception &) {
             return none_expr();
         }
     }
 
-    expr whnf(expr const & e, justification const & j, bool relax, buffer<constraint> & cs) {
+    expr whnf(expr const & e, justification const & j, buffer<constraint> & cs) {
         constraint_seq _cs;
-        expr r = whnf(e, relax, _cs);
+        expr r = whnf(e, _cs);
         to_buffer(_cs, j, cs);
         return r;
     }
 
-    expr flex_rigid_whnf(expr const & e, justification const & j, bool relax, buffer<constraint> & cs) {
+    expr flex_rigid_whnf(expr const & e, justification const & j, buffer<constraint> & cs) {
         if (m_config.m_computation) {
-            return whnf(e, j, relax, cs);
+            return whnf(e, j, cs);
         } else {
             constraint_seq _cs;
             expr r = m_flex_rigid_tc->whnf(e, _cs);
@@ -677,21 +669,19 @@ struct unifier_fn {
        The type of lhs and rhs are inferred, and is_def_eq is invoked.
 
        Any other constraint that contains \c m is revisited
-
-       \remark If relax is true then opaque definitions from the main module are treated as transparent.
     */
-    bool assign(expr const & lhs, expr const & m, buffer<expr> const & args, expr const & rhs, justification const & j, bool relax) {
+    bool assign(expr const & lhs, expr const & m, buffer<expr> const & args, expr const & rhs, justification const & j) {
         lean_assert(is_metavar(m));
         lean_assert(!in_conflict());
         m_subst.assign(m, args, rhs, j);
         constraint_seq cs;
-        auto lhs_type = infer(lhs, relax, cs);
-        auto rhs_type = infer(rhs, relax, cs);
+        auto lhs_type = infer(lhs, cs);
+        auto rhs_type = infer(rhs, cs);
         if (lhs_type && rhs_type) {
             if (!process_constraints(cs, j))
                 return false;
             justification new_j = mk_assign_justification(m, *lhs_type, *rhs_type, j);
-            if (!is_def_eq(*lhs_type, *rhs_type, new_j, relax))
+            if (!is_def_eq(*lhs_type, *rhs_type, new_j))
                 return false;
         } else {
             set_conflict(j);
@@ -754,7 +744,7 @@ struct unifier_fn {
        The method returns \c Failed if \c rhs contains <tt>?m</tt>, or it contains a local constant not in <tt>{l_1, ..., l_n}</tt>.
        Otherwise, it returns \c Continue.
     */
-    status process_metavar_eq(expr const & lhs, expr const & rhs, justification const & j, bool relax) {
+    status process_metavar_eq(expr const & lhs, expr const & rhs, justification const & j) {
         if (!is_meta(lhs))
             return Continue;
         buffer<expr> locals;
@@ -778,9 +768,9 @@ struct unifier_fn {
                     return true;
                 return false;
             };
-            expr rhs_n = normalize(*m_tc[relax], rhs, is_target_fn, cs);
+            expr rhs_n = normalize(*m_tc, rhs, is_target_fn, cs);
             if (rhs != rhs_n && process_constraints(cs))
-                return process_metavar_eq(lhs, rhs_n, j, relax);
+                return process_metavar_eq(lhs, rhs_n, j);
         }
         switch (status) {
         case occurs_check_status::FailLocal:
@@ -793,7 +783,7 @@ struct unifier_fn {
             return Continue;
         case occurs_check_status::Ok:
             lean_assert(!m_subst.is_assigned(*m));
-            if (assign(lhs, *m, locals, rhs, j, relax)) {
+            if (assign(lhs, *m, locals, rhs, j)) {
                 return Solved;
             } else {
                 return Failed;
@@ -803,8 +793,7 @@ struct unifier_fn {
     }
 
     optional<declaration> is_delta(expr const & e) {
-        bool relax_opaque = true;
-        return m_tc[relax_opaque]->is_delta(e);
+        return m_tc->is_delta(e);
     }
 
     /** \brief Return true if lhs and rhs are of the form (f ...) where f can be expanded */
@@ -827,8 +816,7 @@ struct unifier_fn {
             expr rhs = rhs_jst.first;
             if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c)) {
                 return mk_pair(mk_eq_cnstr(lhs, rhs,
-                                           mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second),
-                                           relax_main_opaque(c)),
+                                           mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second)),
                                true);
             }
         } else if (is_level_eq_cnstr(c)) {
@@ -849,20 +837,19 @@ struct unifier_fn {
         expr const & lhs = cnstr_lhs_expr(c);
         expr const & rhs = cnstr_rhs_expr(c);
         justification const & jst = c.get_justification();
-        bool relax = relax_main_opaque(c);
 
         if (lhs == rhs)
             return Solved; // trivial constraint
 
         // Update justification using the justification of the instantiated metavariables
         if (!has_metavar(lhs) && !has_metavar(rhs)) {
-            return is_def_eq(lhs, rhs, jst, relax) ? Solved : Failed;
+            return is_def_eq(lhs, rhs, jst) ? Solved : Failed;
         }
 
         // Handle higher-order pattern matching.
-        status st = process_metavar_eq(lhs, rhs, jst, relax);
+        status st = process_metavar_eq(lhs, rhs, jst);
         if (st != Continue) return st;
-        st = process_metavar_eq(rhs, lhs, jst, relax);
+        st = process_metavar_eq(rhs, lhs, jst);
         if (st != Continue) return st;
 
         return Continue;
@@ -909,11 +896,11 @@ struct unifier_fn {
         expr lhs = instantiate_meta(cnstr_lhs_expr(c), j);
         expr rhs = instantiate_meta(cnstr_rhs_expr(c), j);
         if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c))
-            return is_def_eq(lhs, rhs, j, relax_main_opaque(c)) ? Solved : Failed;
+            return is_def_eq(lhs, rhs, j) ? Solved : Failed;
         lhs = instantiate_meta_args(lhs, j);
         rhs = instantiate_meta_args(rhs, j);
         if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c))
-            return is_def_eq(lhs, rhs, j, relax_main_opaque(c)) ? Solved : Failed;
+            return is_def_eq(lhs, rhs, j) ? Solved : Failed;
         return Continue;
     }
 
@@ -957,7 +944,6 @@ struct unifier_fn {
 
         expr const & lhs = cnstr_lhs_expr(c);
         expr const & rhs = cnstr_rhs_expr(c);
-        bool relax = relax_main_opaque(c);
 
         if (is_eq_deltas(lhs, rhs)) {
             // we need to create a backtracking point for this one
@@ -967,9 +953,9 @@ struct unifier_fn {
             unsigned cidx = add_cnstr(c, cnstr_group::FlexFlex);
             add_meta_occ(lhs, cidx);
             add_meta_occ(rhs, cidx);
-        } else if (m_tc[relax]->may_reduce_later(lhs) ||
-                   m_tc[relax]->may_reduce_later(rhs) ||
-                   m_plugin->delay_constraint(*m_tc[relax], c)) {
+        } else if (m_tc->may_reduce_later(lhs) ||
+                   m_tc->may_reduce_later(rhs) ||
+                   m_plugin->delay_constraint(*m_tc, c)) {
             unsigned cidx = add_cnstr(c, cnstr_group::PluginDelayed);
             add_meta_occs(lhs, cidx);
             add_meta_occs(rhs, cidx);
@@ -1078,9 +1064,8 @@ struct unifier_fn {
                 // should infer it, process generated
                 // constraints and save the result in
                 // m_type_map.
-                bool relax = relax_main_opaque(c);
                 constraint_seq cs;
-                optional<expr> t = infer(m, relax, cs);
+                optional<expr> t = infer(m, cs);
                 if (!t) {
                     set_conflict(c.get_justification());
                     return false;
@@ -1237,8 +1222,7 @@ struct unifier_fn {
             return lazy_list<constraints>();
         justification const & j = c.get_justification();
         constraint_seq cs;
-        bool relax = relax_main_opaque(c);
-        auto fcs = m_tc[relax]->is_def_eq(f_lhs, f_rhs, j);
+        auto fcs = m_tc->is_def_eq(f_lhs, f_rhs, j);
         if (!fcs.first)
             return lazy_list<constraints>();
         cs = fcs.second;
@@ -1248,7 +1232,7 @@ struct unifier_fn {
         if (args_lhs.size() != args_rhs.size())
             return lazy_list<constraints>();
         for (unsigned i = 0; i < args_lhs.size(); i++) {
-            auto acs = m_tc[relax]->is_def_eq(args_lhs[i], args_rhs[i], j);
+            auto acs = m_tc->is_def_eq(args_lhs[i], args_rhs[i], j);
             if (!acs.first)
                 return lazy_list<constraints>();
             cs = acs.second + cs;
@@ -1257,9 +1241,8 @@ struct unifier_fn {
     }
 
     bool process_plugin_constraint(constraint const & c) {
-        bool relax = relax_main_opaque(c);
         lean_assert(!is_choice_cnstr(c));
-        lazy_list<constraints> alts = m_plugin->solve(*m_tc[relax], c, m_ngen.mk_child());
+        lazy_list<constraints> alts = m_plugin->solve(*m_tc, c, m_ngen.mk_child());
         alts = append(alts, process_const_const_cnstr(c));
         return process_lazy_constraints(alts, c.get_justification());
     }
@@ -1274,10 +1257,9 @@ struct unifier_fn {
             m_owned_map.erase(mlocal_name(get_app_fn(m)));
         }
         expr m_type;
-        bool relax = relax_main_opaque(c);
 
         constraint_seq cs;
-        if (auto type = infer(m, relax, cs)) {
+        if (auto type = infer(m, cs)) {
             m_type = *type;
             if (!process_constraints(cs))
                 return false;
@@ -1313,12 +1295,11 @@ struct unifier_fn {
         expr lhs_fn     = get_app_rev_args(lhs, lhs_args);
         expr rhs_fn     = get_app_rev_args(rhs, rhs_args);
         declaration d   = *m_env.find(const_name(lhs_fn));
-        bool relax = relax_main_opaque(c);
         expr lhs_fn_val = instantiate_value_univ_params(d, const_levels(lhs_fn));
         expr rhs_fn_val = instantiate_value_univ_params(d, const_levels(rhs_fn));
         expr t = apply_beta(lhs_fn_val, lhs_args.size(), lhs_args.data());
         expr s = apply_beta(rhs_fn_val, rhs_args.size(), rhs_args.data());
-        auto dcs = m_tc[relax]->is_def_eq(t, s, j);
+        auto dcs = m_tc->is_def_eq(t, s, j);
         if (dcs.first) {
             constraints cnstrs = dcs.second.to_list();
             return process_constraints(cnstrs, extra_j);
@@ -1371,7 +1352,6 @@ struct unifier_fn {
             return unfold_delta(c, justification());
 
         justification a;
-        bool relax = relax_main_opaque(c);
         if (m_config.m_kind == unifier_kind::Liberal &&
             (m_config.m_computation || module::is_definition(m_env, d.get_name()) || is_at_least_quasireducible(m_env, d.get_name()))) {
             // add case_split for t =?= s
@@ -1393,7 +1373,7 @@ struct unifier_fn {
         unsigned i = lhs_args.size();
         while (i > 0) {
             --i;
-            if (!is_def_eq(lhs_args[i], rhs_args[i], new_j, relax))
+            if (!is_def_eq(lhs_args[i], rhs_args[i], new_j))
                 return false;
         }
         return true;
@@ -1429,7 +1409,6 @@ struct unifier_fn {
         expr const &          m;
         expr const &          rhs;
         justification         j;
-        bool                  relax;
         buffer<constraints> & alts; // result: alternatives
         bool                  imitation_only; // if true, then only imitation step is used
 
@@ -1439,12 +1418,12 @@ struct unifier_fn {
         bool pattern() const { return u.m_config.m_pattern; }
 
         type_checker & tc() {
-            return *u.m_tc[relax];
+            return *u.m_tc;
         }
 
         type_checker & restricted_tc() {
             if (u.m_config.m_computation)
-                return *u.m_tc[relax];
+                return *u.m_tc;
             else
                 return *u.m_flex_rigid_tc;
         }
@@ -1529,7 +1508,7 @@ struct unifier_fn {
             expr const & mtype = mlocal_type(m);
             constraint_seq cs;
             expr new_mtype = ensure_sufficient_args(mtype, cs);
-            cs = cs + mk_eq_cnstr(m, mk_lambda_for(new_mtype, rhs), j, relax);
+            cs = cs + mk_eq_cnstr(m, mk_lambda_for(new_mtype, rhs), j);
             alts.push_back(cs.to_list());
         }
 
@@ -1570,7 +1549,7 @@ struct unifier_fn {
             if (tc().is_def_eq_types(marg, rhs, j, cs) &&
                 restricted_is_def_eq(marg, rhs, j, cs)) {
                 expr v = mk_lambda_for(new_mtype, mk_var(vidx));
-                cs = cs + mk_eq_cnstr(m, v, j, relax);
+                cs = cs + mk_eq_cnstr(m, v, j);
                 alts.push_back(cs.to_list());
             }
         }
@@ -1610,7 +1589,7 @@ struct unifier_fn {
                     constraint_seq cs;
                     auto new_mtype = ensure_sufficient_args(mtype, cs);
                     expr v = mk_lambda_for(new_mtype, mk_var(vidx));
-                    cs = cs + mk_eq_cnstr(m, v, j, relax);
+                    cs = cs + mk_eq_cnstr(m, v, j);
                     alts.push_back(cs.to_list());
                     if (cheap())
                         return;
@@ -1694,12 +1673,12 @@ struct unifier_fn {
             if (context_check(type, locals)) {
                 expr maux    = mk_metavar(u.m_ngen.next(), Pi(locals, type));
                 // std::cout << "  >> " << maux << " : " << mlocal_type(maux) << "\n";
-                cs = mk_eq_cnstr(mk_app(maux, margs), arg, j, relax) + cs;
+                cs = mk_eq_cnstr(mk_app(maux, margs), arg, j) + cs;
                 return mk_app(maux, locals);
             } else {
                 expr maux_type   = mk_metavar(u.m_ngen.next(), Pi(locals, mk_sort(mk_meta_univ(u.m_ngen.next()))));
                 expr maux        = mk_metavar(u.m_ngen.next(), Pi(locals, mk_app(maux_type, locals)));
-                cs = mk_eq_cnstr(mk_app(maux, margs), arg, j, relax) + cs;
+                cs = mk_eq_cnstr(mk_app(maux, margs), arg, j) + cs;
                 return mk_app(maux, locals);
             }
         }
@@ -1719,7 +1698,7 @@ struct unifier_fn {
                 }
             } catch (exception&) {}
             expr v = Fun(locals, mk_app(f, sargs));
-            cs += mk_eq_cnstr(m, v, j, relax);
+            cs += mk_eq_cnstr(m, v, j);
             alts.push_back(cs.to_list());
         }
 
@@ -1797,7 +1776,7 @@ struct unifier_fn {
                 expr binding   = is_pi(rhs) ? Pi(local, B) : Fun(local, B);
                 locals.pop_back();
                 expr v         = Fun(locals, binding);
-                cs += mk_eq_cnstr(m, v, j, relax);
+                cs += mk_eq_cnstr(m, v, j);
                 alts.push_back(cs.to_list());
             } catch (exception&) {}
             margs.pop_back();
@@ -1805,9 +1784,9 @@ struct unifier_fn {
 
     public:
         flex_rigid_core_fn(unifier_fn & _u, expr const & _lhs, expr const & _rhs,
-                           justification const & _j, bool _relax, buffer<constraints> & _alts,
+                           justification const & _j, buffer<constraints> & _alts,
                            bool _imitation_only):
-            u(_u), lhs(_lhs), m(get_app_args(lhs, margs)), rhs(_rhs), j(_j), relax(_relax), alts(_alts),
+            u(_u), lhs(_lhs), m(get_app_args(lhs, margs)), rhs(_rhs), j(_j), alts(_alts),
             imitation_only(_imitation_only) {}
 
         void operator()() {
@@ -1838,9 +1817,9 @@ struct unifier_fn {
         }
     };
 
-    void process_flex_rigid_core(expr const & lhs, expr const & rhs, justification const & j, bool relax,
+    void process_flex_rigid_core(expr const & lhs, expr const & rhs, justification const & j,
                                  buffer<constraints> & alts, bool imitation_only) {
-        flex_rigid_core_fn(*this, lhs, rhs, j, relax, alts, imitation_only)();
+        flex_rigid_core_fn(*this, lhs, rhs, j, alts, imitation_only)();
     }
 
     /** \brief When lhs is an application (f ...), make sure that if any argument that is reducible to a
@@ -1849,14 +1828,14 @@ struct unifier_fn {
         \remark We store auxiliary constraints created in the reductions in \c aux. We return the new
         "reduce" application.
     */
-    expr expose_local_args(expr const & lhs, justification const & j, bool relax, buffer<constraint> & aux) {
+    expr expose_local_args(expr const & lhs, justification const & j, buffer<constraint> & aux) {
         buffer<expr> margs;
         expr m        = get_app_args(lhs, margs);
         bool modified = false;
         for (expr & marg : margs) {
             // Make sure that if marg is reducible to a local constant, then it is replaced with it.
             if (!is_local(marg)) {
-                expr new_marg = whnf(marg, j, relax, aux);
+                expr new_marg = whnf(marg, j, aux);
                 if (is_local(new_marg)) {
                     marg     = new_marg;
                     modified = true;
@@ -1866,14 +1845,14 @@ struct unifier_fn {
         return modified ? mk_app(m, margs) : lhs;
     }
 
-    optional<expr> expand_rhs(expr const & rhs, bool relax) {
+    optional<expr> expand_rhs(expr const & rhs) {
         buffer<expr> args;
         expr const & f = get_app_rev_args(rhs, args);
         lean_assert(!is_local(f) && !is_constant(f) && !is_var(f) && !is_metavar(f));
         if (is_lambda(f)) {
             return some_expr(apply_beta(f, args.size(), args.data()));
         } else if (is_macro(f)) {
-            if (optional<expr> new_f = m_tc[relax]->expand_macro(f))
+            if (optional<expr> new_f = m_tc->expand_macro(f))
                 return some_expr(mk_rev_app(*new_f, args.size(), args.data()));
         }
         return none_expr();
@@ -1907,42 +1886,42 @@ struct unifier_fn {
     }
 
     /** \brief Process a flex rigid constraint */
-    bool process_flex_rigid(expr lhs, expr const & rhs, justification const & j, bool relax) {
+    bool process_flex_rigid(expr lhs, expr const & rhs, justification const & j) {
         lean_assert(is_meta(lhs));
         lean_assert(!is_meta(rhs));
         if (is_app(rhs)) {
             expr const & f = get_app_fn(rhs);
             if (!is_local(f) && !is_constant(f)) {
-                if (auto new_rhs = expand_rhs(rhs, relax)) {
+                if (auto new_rhs = expand_rhs(rhs)) {
                     lean_assert(*new_rhs != rhs);
-                    return is_def_eq(lhs, *new_rhs, j, relax);
+                    return is_def_eq(lhs, *new_rhs, j);
                 } else {
                     return false;
                 }
             }
         } else if (is_macro(rhs)) {
-            if (auto new_rhs = expand_rhs(rhs, relax)) {
+            if (auto new_rhs = expand_rhs(rhs)) {
                 lean_assert(*new_rhs != rhs);
-                return is_def_eq(lhs, *new_rhs, j, relax);
+                return is_def_eq(lhs, *new_rhs, j);
             } else {
                 return false;
             }
         }
 
         buffer<constraint> aux;
-        lhs = expose_local_args(lhs, j, relax, aux);
+        lhs = expose_local_args(lhs, j, aux);
         buffer<constraints> alts;
-        process_flex_rigid_core(lhs, rhs, j, relax, alts, false);
+        process_flex_rigid_core(lhs, rhs, j, alts, false);
         append_auxiliary_constraints(alts, to_list(aux.begin(), aux.end()));
         if (use_flex_rigid_whnf_split(lhs, rhs)) {
-            expr rhs_whnf = flex_rigid_whnf(rhs, j, relax, aux);
+            expr rhs_whnf = flex_rigid_whnf(rhs, j, aux);
             if (rhs_whnf != rhs) {
                 if (is_meta(rhs_whnf)) {
                     // it become a flex-flex constraint
-                    alts.push_back(constraints(mk_eq_cnstr(lhs, rhs_whnf, j, relax)));
+                    alts.push_back(constraints(mk_eq_cnstr(lhs, rhs_whnf, j)));
                 } else {
                     buffer<constraints> alts2;
-                    process_flex_rigid_core(lhs, rhs_whnf, j, relax, alts2, true);
+                    process_flex_rigid_core(lhs, rhs_whnf, j, alts2, true);
                     append_auxiliary_constraints(alts2, to_list(aux.begin(), aux.end()));
                     alts.append(alts2);
                 }
@@ -1975,11 +1954,10 @@ struct unifier_fn {
         lean_assert(is_flex_rigid(c));
         expr lhs   = cnstr_lhs_expr(c);
         expr rhs   = cnstr_rhs_expr(c);
-        bool relax = relax_main_opaque(c);
         if (is_meta(lhs))
-            return process_flex_rigid(lhs, rhs, c.get_justification(), relax);
+            return process_flex_rigid(lhs, rhs, c.get_justification());
         else
-            return process_flex_rigid(rhs, lhs, c.get_justification(), relax);
+            return process_flex_rigid(rhs, lhs, c.get_justification());
     }
 
     void postpone(constraint const & c) {
@@ -2019,9 +1997,9 @@ struct unifier_fn {
                 break;
         if (i == min_sz) {
             if (lhs_args.size() >= rhs_args.size()) {
-                return assign(lhs, ml, lhs_args, rhs, c.get_justification(), relax_main_opaque(c));
+                return assign(lhs, ml, lhs_args, rhs, c.get_justification());
             } else {
-                return assign(rhs, mr, rhs_args, lhs, c.get_justification(), relax_main_opaque(c));
+                return assign(rhs, mr, rhs_args, lhs, c.get_justification());
             }
         } else {
             discard(c);
@@ -2263,7 +2241,7 @@ struct unifier_fn {
                 if (is_delta_cnstr(c)) {
                     return process_delta(c);
                 } else if (modified) {
-                    return is_def_eq(cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification(), relax_main_opaque(c));
+                    return is_def_eq(cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification());
                 } else if (auto d = is_owned(c)) {
                     // Metavariable in the constraint is owned by choice constraint.
                     // choice constraint was postponed... since c was not modifed
@@ -2353,13 +2331,13 @@ unify_result_seq unify(environment const & env,  unsigned num_cs, constraint con
 }
 
 unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
-                       bool relax, substitution const & s, unifier_config const & cfg) {
+                       substitution const & s, unifier_config const & cfg) {
     substitution new_s = s;
     expr _lhs = new_s.instantiate(lhs);
     expr _rhs = new_s.instantiate(rhs);
     auto u = std::make_shared<unifier_fn>(env, 0, nullptr, ngen, new_s, cfg);
     constraint_seq cs;
-    if (!u->m_tc[relax]->is_def_eq(_lhs, _rhs, justification(), cs) || !u->process_constraints(cs)) {
+    if (!u->m_tc->is_def_eq(_lhs, _rhs, justification(), cs) || !u->process_constraints(cs)) {
         return unify_result_seq();
     } else {
         return unify(u);
@@ -2485,13 +2463,13 @@ static int unify(lua_State * L) {
     unify_result_seq r;
     environment const & env = to_environment(L, 1);
     if (is_expr(L, 2)) {
-        if (nargs == 7)
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5), to_substitution(L, 6),
-                      unifier_config(to_options(L, 7)));
-        else if (nargs == 6)
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5), to_substitution(L, 6));
+        if (nargs == 6)
+            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5),
+                      unifier_config(to_options(L, 6)));
+        else if (nargs == 5)
+            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5));
         else
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5));
+            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4));
     } else {
         buffer<constraint> cs;
         to_constraint_buffer(L, 2, cs);
@@ -2539,7 +2517,7 @@ void initialize_unifier() {
     register_bool_option(*g_unifier_nonchronological, LEAN_DEFAULT_UNIFIER_NONCHRONOLOGICAL,
                          "(unifier) enable/disable nonchronological backtracking in the unifier (this option is only available for debugging and benchmarking purposes, and running experiments)");
 
-    g_dont_care_cnstr = new constraint(mk_eq_cnstr(expr(), expr(), justification(), false));
+    g_dont_care_cnstr = new constraint(mk_eq_cnstr(expr(), expr(), justification()));
     g_tmp_prefix      = new name(name::mk_internal_unique_name());
 }
 
diff --git a/src/library/unifier.h b/src/library/unifier.h
index 446749930..1730daeee 100644
--- a/src/library/unifier.h
+++ b/src/library/unifier.h
@@ -77,7 +77,7 @@ typedef lazy_list<pair<substitution, constraints>> unify_result_seq;
 unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen,
                        substitution const & s = substitution(), unifier_config const & c = unifier_config());
 unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
-                       bool relax_main_opaque, substitution const & s = substitution(), unifier_config const & c = unifier_config());
+                       substitution const & s = substitution(), unifier_config const & c = unifier_config());
 
 /**
     The unifier divides the constraints in 9 groups: Simple, Basic, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance,
diff --git a/src/library/update_declaration.cpp b/src/library/update_declaration.cpp
index 2965e9c1b..b22aa9e2f 100644
--- a/src/library/update_declaration.cpp
+++ b/src/library/update_declaration.cpp
@@ -31,7 +31,7 @@ static declaration update_declaration(declaration d, optional<level_param_names>
             return mk_theorem(d.get_name(), _ps, _type, _value);
         else
             return mk_definition(d.get_name(), _ps, _type, _value, d.is_opaque(),
-                                 d.get_weight(), d.get_module_idx(), d.use_conv_opt());
+                                 d.get_weight(), d.use_conv_opt());
     }
 }
 
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 27a3e6455..b17a1778c 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -627,8 +627,7 @@ constraint instantiate_metavars(constraint const & c, substitution & s) {
     case constraint_kind::Eq:
         return mk_eq_cnstr(s.instantiate_all(cnstr_lhs_expr(c)),
                            s.instantiate_all(cnstr_rhs_expr(c)),
-                           c.get_justification(),
-                           relax_main_opaque(c));
+                           c.get_justification());
     case constraint_kind::LevelEq:
         return mk_level_eq_cnstr(s.instantiate(cnstr_lhs_level(c)), s.instantiate(cnstr_rhs_level(c)), c.get_justification());
     case constraint_kind::Choice: {
@@ -642,7 +641,7 @@ constraint instantiate_metavars(constraint const & c, substitution & s) {
         return mk_choice_cnstr(mk_app(mvar, args),
                                cnstr_choice_fn(c),
                                cnstr_delay_factor_core(c),
-                               cnstr_is_owner(c), c.get_justification(), relax_main_opaque(c));
+                               cnstr_is_owner(c), c.get_justification());
     }}
     lean_unreachable(); // LCOV_EXCL_LINE
 }
diff --git a/src/tests/library/unifier.cpp b/src/tests/library/unifier.cpp
index e97192d0c..96c65ee87 100644
--- a/src/tests/library/unifier.cpp
+++ b/src/tests/library/unifier.cpp
@@ -23,7 +23,7 @@ static void tst1() {
     expr m  = mk_metavar("m", A);
     expr t1 = mk_app(f, m, m);
     expr t2 = mk_app(f, a, b);
-    auto r = unify(env, t1, t2, ngen, false);
+    auto r = unify(env, t1, t2, ngen);
     lean_assert(!r.pull());
 }
 
diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean
index 296dc13c4..ef91357f4 100644
--- a/tests/lean/run/match1.lean
+++ b/tests/lean/run/match1.lean
@@ -6,7 +6,7 @@ definition two2 : nat := succ (succ (zero))
 constant f      : nat → nat → nat
 
 (*
-local tc     = type_checker_with_hints(get_env(), true)
+local tc     = type_checker_with_hints(get_env())
 local plugin = whnf_match_plugin(tc)
 function tst_match(p, t)
    local r1, r2   = match(p, t, plugin)
diff --git a/tests/lean/run/match2.lean b/tests/lean/run/match2.lean
index b0e3368cb..508767041 100644
--- a/tests/lean/run/match2.lean
+++ b/tests/lean/run/match2.lean
@@ -8,7 +8,7 @@ constant g : nat → nat → nat
 constants a b : nat
 
 (*
-local tc     = type_checker_with_hints(get_env(), true)
+local tc     = type_checker_with_hints(get_env())
 local plugin = whnf_match_plugin(tc)
 function tst_match(p, t)
    local r1, r2   = match(p, t, plugin)
diff --git a/tests/lua/def1.lua b/tests/lua/def1.lua
index d8bc10ca9..508fc567f 100644
--- a/tests/lua/def1.lua
+++ b/tests/lua/def1.lua
@@ -29,25 +29,21 @@ assert(th2:name() == name("t2"))
 local d  = mk_definition("d1", A, B)
 assert(d:is_definition())
 assert(not d:is_theorem())
-assert(d:opaque())
 assert(d:weight() == 0)
-assert(d:module_idx() == 0)
 assert(d:use_conv_opt())
 assert(d:name() == name("d1"))
 assert(d:value() == B)
 local d2  = mk_definition("d2", A, B, nil)
-local d3  = mk_definition("d3", A, B, {opaque=false, weight=100, module_idx=10, use_conv_opt=false})
+local d3  = mk_definition("d3", A, B, {opaque=false, weight=100, use_conv_opt=false})
 assert(not d3:opaque())
 assert(d3:weight() == 100)
-assert(d3:module_idx() == 10)
 assert(not d3:use_conv_opt())
 local env = bare_environment()
 local d4  = mk_definition(env, "bool", Type, Prop)
 assert(d4:weight() == 1)
-local d5  = mk_definition(env, "bool", Type, Prop, {opaque=false, weight=100, module_idx=3, use_conv_opt=true})
+local d5  = mk_definition(env, "bool", Type, Prop, {opaque=false, weight=100, use_conv_opt=true})
 assert(not d5:opaque())
 assert(d5:weight() == 1)
-assert(d5:module_idx() == 3)
 assert(d5:use_conv_opt())
 local d6  = mk_definition("d6", {"l1", "l2"}, A, B, {opaque=true, weight=5})
 assert(d6:type() == A)