diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 362ae622c..f452933ec 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -12,7 +12,7 @@
     "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "constant" "constants"
     "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises"
     "print" "theorem" "example" "abbreviation"
-    "context" "open" "as" "export" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
+    "open" "as" "export" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
     "alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix"
     "calc_trans" "calc_subst" "calc_refl" "calc_symm" "match"
     "infix" "infixl" "infixr" "notation" "eval" "check" "coercion" "end"
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index b09f8eaa3..2122b1bf3 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -252,15 +252,6 @@ environment section_cmd(parser & p) {
     return push_scope(p.env(), p.ios(), scope_kind::Section, n);
 }
 
-environment context_cmd(parser & p) {
-    name n;
-    if (p.curr_is_identifier())
-        n = p.check_atomic_id_next("invalid context, atomic identifier expected");
-    bool save_options = true;
-    p.push_local_scope(save_options);
-    return push_scope(p.env(), p.ios(), scope_kind::Context, n);
-}
-
 environment namespace_cmd(parser & p) {
     auto pos = p.pos();
     name n = p.check_atomic_id_next("invalid namespace declaration, atomic identifier expected");
@@ -274,7 +265,7 @@ static environment redeclare_aliases(environment env, parser & p,
                                      list<pair<name, level>> old_level_entries,
                                      list<pair<name, expr>> old_entries) {
     environment const & old_env = p.env();
-    if (!in_context(old_env) && !in_section(old_env))
+    if (!in_section(old_env))
         return env;
     list<pair<name, expr>> new_entries = p.get_local_entries();
     buffer<pair<name, expr>> to_redeclare;
@@ -695,7 +686,6 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("exit",          "exit", exit_cmd));
     add_cmd(r, cmd_info("print",         "print a string", print_cmd));
     add_cmd(r, cmd_info("section",       "open a new section", section_cmd));
-    add_cmd(r, cmd_info("context",       "open a new context", context_cmd));
     add_cmd(r, cmd_info("namespace",     "open a new namespace", namespace_cmd));
     add_cmd(r, cmd_info("end",           "close the current namespace/section", end_scoped_cmd));
     add_cmd(r, cmd_info("check",         "type check given expression, and display its type", check_cmd));
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 96fa8fe0c..a5013f66c 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -37,7 +37,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 static environment declare_universe(parser & p, environment env, name const & n, bool local) {
-    if (in_context(env) || local) {
+    if (local) {
         p.add_local_level(n, mk_param_univ(n), local);
     } else {
         name const & ns = get_namespace(env);
@@ -125,7 +125,7 @@ static environment declare_var(parser & p, environment env,
     if (_bi) bi = *_bi;
     if (k == variable_kind::Parameter || k == variable_kind::Variable) {
         if (k == variable_kind::Parameter) {
-            check_in_context_or_section(p);
+            check_in_section(p);
             check_parameter_type(p, n, type, pos);
         }
         if (p.get_local(n))
@@ -172,13 +172,13 @@ optional<binder_info> parse_binder_info(parser & p, variable_kind k) {
 }
 
 static void check_variable_kind(parser & p, variable_kind k) {
-    if (in_context(p.env()) || in_section(p.env())) {
+    if (in_section(p.env())) {
         if (k == variable_kind::Axiom || k == variable_kind::Constant)
-            throw parser_error("invalid declaration, 'constant/axiom' cannot be used in sections/contexts",
+            throw parser_error("invalid declaration, 'constant/axiom' cannot be used in sections",
                                p.pos());
-    } else if (!in_section(p.env()) && !in_context(p.env()) && k == variable_kind::Parameter) {
+    } else if (!in_section(p.env()) && k == variable_kind::Parameter) {
         throw parser_error("invalid declaration, 'parameter/hypothesis/conjecture' "
-                           "can only be used in contexts and sections", p.pos());
+                           "can only be used in sections", p.pos());
     }
 }
 
@@ -374,10 +374,7 @@ struct decl_attributes {
                 m_is_instance = true;
                 p.next();
             } else if (p.curr_is_token(get_coercion_tk())) {
-                auto pos = p.pos();
                 p.next();
-                if (in_context(p.env()) && m_persistent)
-                    throw parser_error("invalid '[coercion]' attribute, (non local) coercions cannot be defined in contexts", pos);
                 m_is_coercion = true;
             } else if (p.curr_is_token(get_reducible_tk())) {
                 if (m_is_irreducible || m_is_semireducible || m_is_quasireducible)
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index 7eca1a303..2d20b4ffc 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -627,7 +627,7 @@ struct notation_modifiers {
 static environment notation_cmd_core(parser & p, bool overload, bool reserve, bool persistent) {
     notation_modifiers mods;
     mods.parse(p);
-    flet<bool> set_allow_local(g_allow_local, in_context(p.env()) || !persistent);
+    flet<bool> set_allow_local(g_allow_local, !persistent);
     environment env = p.env();
     buffer<token_entry> new_tokens;
     auto ne = parse_notation_core(p, overload, reserve, new_tokens, mods.m_parse_only);
@@ -640,7 +640,7 @@ static environment notation_cmd_core(parser & p, bool overload, bool reserve, bo
 static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, bool reserve, bool persistent) {
     notation_modifiers mods;
     mods.parse(p);
-    flet<bool> set_allow_local(g_allow_local, in_context(p.env()) || !persistent);
+    flet<bool> set_allow_local(g_allow_local, !persistent);
     auto nt = parse_mixfix_notation(p, k, overload, reserve, mods.m_parse_only);
     environment env = p.env();
     if (nt.second)
@@ -650,35 +650,35 @@ static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, bool res
 }
 
 static environment notation_cmd(parser & p) {
-    bool overload = !in_context(p.env());
+    bool overload = true;
     bool reserve  = false;
     bool persistent = true;
     return notation_cmd_core(p, overload, reserve, persistent);
 }
 
 static environment infixl_cmd(parser & p) {
-    bool overload = !in_context(p.env());
+    bool overload = true;
     bool reserve  = false;
     bool persistent = true;
     return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve, persistent);
 }
 
 static environment infixr_cmd(parser & p) {
-    bool overload = !in_context(p.env());
+    bool overload = true;
     bool reserve  = false;
     bool persistent = true;
     return mixfix_cmd(p, mixfix_kind::infixr, overload, reserve, persistent);
 }
 
 static environment postfix_cmd(parser & p) {
-    bool overload = !in_context(p.env());
+    bool overload = true;
     bool reserve  = false;
     bool persistent = true;
     return mixfix_cmd(p, mixfix_kind::postfix, overload, reserve, persistent);
 }
 
 static environment prefix_cmd(parser & p) {
-    bool overload = !in_context(p.env());
+    bool overload = true;
     bool reserve  = false;
     bool persistent = true;
     return mixfix_cmd(p, mixfix_kind::prefix, overload, reserve, persistent);
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 63eb36a65..1969aa91a 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -457,7 +457,7 @@ void parser::push_local_scope(bool save_options) {
 
 void parser::pop_local_scope() {
     if (!m_local_level_decls.has_scopes()) {
-        throw parser_error("invalid 'end', there is no open namespace/section/context", pos());
+        throw parser_error("invalid 'end', there is no open namespace/section", pos());
     }
     m_local_level_decls.pop();
     m_local_decls.pop();
@@ -1116,7 +1116,7 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
     if (auto it1 = m_local_decls.find(id)) {
         if (ls && m_undef_id_behavior != undef_id_behavior::AssumeConstant)
             throw parser_error("invalid use of explicit universe parameter, identifier is a variable, "
-                               "parameter or a constant bound to parameters in a section/context", p);
+                               "parameter or a constant bound to parameters in a section", p);
         auto r = copy_with_new_pos(*it1, p);
         save_type_info(r);
         save_identifier_info(p, id);
@@ -1189,7 +1189,7 @@ name parser::check_constant_next(char const * msg) {
     name id = check_id_next(msg);
     expr e  = id_to_expr(id, p);
 
-    if ((in_section(m_env) || in_context(m_env)) && is_as_atomic(e)) {
+    if (in_section(m_env) && is_as_atomic(e)) {
         e = get_app_fn(get_as_atomic_arg(e));
         if (is_explicit(e))
             e = get_explicit_arg(e);
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 962c7c59f..cbf45d72b 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -96,7 +96,7 @@ void init_token_table(token_table & t) {
          "evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-f]", "[unfold-c", "print",
          "end", "namespace", "section", "prelude", "help",
          "import", "inductive", "record", "structure", "module", "universe", "universes", "local",
-         "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
+         "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
          "multiple_instances", "find_decl", "attribute", "persistent",
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 59cb5250b..4b4c6dc72 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -60,14 +60,9 @@ void check_atomic(name const & n) {
         throw exception(sstream() << "invalid declaration name '" << n << "', identifier must be atomic");
 }
 
-void check_in_context(parser const & p) {
-    if (!in_context(p.env()))
-        throw exception(sstream() << "invalid command, it must be used in a (local) context");
-}
-
-void check_in_context_or_section(parser const & p) {
-    if (!in_context(p.env()) && !in_section(p.env()))
-        throw exception(sstream() << "invalid command, it must be used in a (local) context or section");
+void check_in_section(parser const & p) {
+    if (!in_section(p.env()))
+        throw exception(sstream() << "invalid command, it must be used in a section");
 }
 
 bool is_root_namespace(name const & n) {
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index 31a09f7a7..3eebf7216 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -27,8 +27,7 @@ void check_command_period_or_eof(parser const & p);
 /** \brief Throw and error if the current token is not a command, nor an open binder, nor a '.', nor an end-of-file. */
 void check_command_period_open_binder_or_eof(parser const & p);
 void check_atomic(name const & n);
-void check_in_context(parser const & p);
-void check_in_context_or_section(parser const & p);
+void check_in_section(parser const & p);
 bool is_root_namespace(name const & n);
 name remove_root_prefix(name const & n);
 /** \brief Return the local levels in \c ls that are not tagged as variables.
diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp
index e22276413..18165aee7 100644
--- a/src/library/aliases.cpp
+++ b/src/library/aliases.cpp
@@ -25,12 +25,12 @@ static environment update(environment const & env, aliases_ext const & ext);
 
 struct aliases_ext : public environment_extension {
     struct state {
-        bool                  m_in_context;
+        bool                  m_in_section;
         name_map<list<name>>  m_aliases;
         name_map<name>        m_inv_aliases;
         name_map<name>        m_level_aliases;
         name_map<name>        m_inv_level_aliases;
-        state():m_in_context(false) {}
+        state():m_in_section(false) {}
 
         void add_expr_alias(name const & a, name const & e, bool overwrite) {
             auto it = m_aliases.find(a);
@@ -63,7 +63,7 @@ struct aliases_ext : public environment_extension {
         } else {
             state s = head(scopes);
             s.add_expr_alias(a, e, overwrite);
-            if (s.m_in_context) {
+            if (s.m_in_section) {
                 return cons(s, add_expr_alias_rec_core(tail(scopes), a, e, overwrite));
             } else {
                 return cons(s, tail(scopes));
@@ -72,15 +72,15 @@ struct aliases_ext : public environment_extension {
     }
 
     void add_expr_alias_rec(name const & a, name const & e, bool overwrite = false) {
-        if (m_state.m_in_context) {
+        if (m_state.m_in_section) {
             m_scopes = add_expr_alias_rec_core(m_scopes, a, e, overwrite);
         }
         add_expr_alias(a, e, overwrite);
     }
 
-    void push(bool in_context) {
+    void push(bool in_section) {
         m_scopes = cons(m_state, m_scopes);
-        m_state.m_in_context = in_context;
+        m_state.m_in_section = in_section;
     }
 
     void pop() {
@@ -106,7 +106,7 @@ struct aliases_ext : public environment_extension {
         aliases_ext ext = get_extension(env);
         ext.push(k != scope_kind::Namespace);
         environment new_env = update(env, ext);
-        if (!::lean::in_context(new_env) && !::lean::in_section(new_env))
+        if (!::lean::in_section(new_env))
             new_env = add_aliases(new_env, get_namespace(new_env), name());
         return new_env;
     }
diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp
index 3fbb45bbc..975a7f88c 100644
--- a/src/library/scoped_ext.cpp
+++ b/src/library/scoped_ext.cpp
@@ -50,18 +50,9 @@ list<name> const & get_namespaces(environment const & env) {
     return get_extension(env).m_namespaces;
 }
 
-bool in_section_or_context(environment const & env) {
-    scope_mng_ext const & ext = get_extension(env);
-    return !is_nil(ext.m_scope_kinds) && head(ext.m_scope_kinds) != scope_kind::Namespace;
-}
-
-bool in_context(environment const & env) {
-    scope_mng_ext const & ext = get_extension(env);
-    return !is_nil(ext.m_scope_kinds) && head(ext.m_scope_kinds) == scope_kind::Context;
-}
-
 bool in_section(environment const & env) {
-    return in_section_or_context(env) && !in_context(env);
+    scope_mng_ext const & ext = get_extension(env);
+    return !is_nil(ext.m_scope_kinds) && head(ext.m_scope_kinds) == scope_kind::Section;
 }
 
 void get_metaclasses(buffer<name> & r) {
@@ -143,10 +134,8 @@ environment add_namespace(environment const & env, name const & ns) {
 }
 
 environment push_scope(environment const & env, io_state const & ios, scope_kind k, name const & n) {
-    if (k == scope_kind::Namespace && in_section_or_context(env))
-        throw exception("invalid namespace declaration, a namespace cannot be declared inside a section or context");
-    if (k == scope_kind::Section && in_context(env))
-        throw exception("invalid section declaration, a section cannot be declared inside a context");
+    if (k == scope_kind::Namespace && in_section(env))
+        throw exception("invalid namespace declaration, a namespace cannot be declared inside a section");
     name new_n = get_namespace(env);
     if (k == scope_kind::Namespace)
         new_n = new_n + n;
@@ -200,7 +189,7 @@ environment pop_scope_core(environment const & env, io_state const & ios) {
 environment pop_scope(environment const & env, io_state const & ios, name const & n) {
     scope_mng_ext ext = get_extension(env);
     if (is_nil(ext.m_namespaces))
-        throw exception("invalid end of scope, there are no open namespaces/sections/contexts");
+        throw exception("invalid end of scope, there are no open namespaces/sections");
     if (n != head(ext.m_headers))
         throw exception(sstream() << "invalid end of scope, begin/end mistmatch, scope starts with '"
                         << head(ext.m_headers) << "', and ends with '" << n << "'");
@@ -227,7 +216,7 @@ static int using_namespace_objects(lua_State * L) {
 static int push_scope(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 1)
-        return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), scope_kind::Context));
+        return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), scope_kind::Section));
     else if (nargs == 2)
         return push_environment(L, push_scope(to_environment(L, 1), get_io_state(L), scope_kind::Namespace, to_name_ext(L, 2)));
     scope_kind k = static_cast<scope_kind>(lua_tonumber(L, 3));
@@ -253,7 +242,6 @@ void open_scoped_ext(lua_State * L) {
     lua_newtable(L);
     SET_ENUM("Namespace",   scope_kind::Namespace);
     SET_ENUM("Section",     scope_kind::Section);
-    SET_ENUM("Context",     scope_kind::Context);
     lua_setglobal(L, "scope_kind");
 }
 
diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h
index e8c9bd101..76f07c22c 100644
--- a/src/library/scoped_ext.h
+++ b/src/library/scoped_ext.h
@@ -16,7 +16,7 @@ Author: Leonardo de Moura
 #include "library/fingerprint.h"
 
 namespace lean {
-enum class scope_kind { Namespace, Section, Context };
+enum class scope_kind { Namespace, Section };
 typedef environment (*using_namespace_fn)(environment const &, io_state const &, name const &);
 typedef environment (*export_namespace_fn)(environment const &, io_state const &, name const &);
 typedef environment (*push_scope_fn)(environment const &, io_state const &, scope_kind);
@@ -56,7 +56,6 @@ environment add_namespace(environment const & env, name const & ns);
 
 name const & get_namespace(environment const & env);
 list<name> const & get_namespaces(environment const & env);
-bool in_context(environment const & env);
 bool in_section(environment const & env);
 
 /** \brief Check if \c n may be a reference to a namespace, if it is return it.
@@ -234,7 +233,7 @@ public:
         if (auto h = get_fingerprint(e)) {
             env = update_fingerprint(env, *h);
         }
-        if (in_context(env) || !persistent) {
+        if (!persistent) {
             return update(env, get(env)._add_tmp_entry(env, ios, e));
         } else {
             name n = get_namespace(env);
diff --git a/tests/lean/bad_end.lean.expected.out b/tests/lean/bad_end.lean.expected.out
index 66ed1a0d4..7dbee852d 100644
--- a/tests/lean/bad_end.lean.expected.out
+++ b/tests/lean/bad_end.lean.expected.out
@@ -1 +1 @@
-bad_end.lean:1:4: error: invalid 'end', there is no open namespace/section/context
+bad_end.lean:1:4: error: invalid 'end', there is no open namespace/section
diff --git a/tests/lean/sec3.lean.expected.out b/tests/lean/sec3.lean.expected.out
index 79c5acc7a..e51c5eb84 100644
--- a/tests/lean/sec3.lean.expected.out
+++ b/tests/lean/sec3.lean.expected.out
@@ -1 +1 @@
-sec3.lean:5:8: error: invalid use of explicit universe parameter, identifier is a variable, parameter or a constant bound to parameters in a section/context
+sec3.lean:5:8: error: invalid use of explicit universe parameter, identifier is a variable, parameter or a constant bound to parameters in a section
diff --git a/tests/lean/t3.lean.expected.out b/tests/lean/t3.lean.expected.out
index 6432d99de..b480e1388 100644
--- a/tests/lean/t3.lean.expected.out
+++ b/tests/lean/t3.lean.expected.out
@@ -5,7 +5,7 @@ Type
 t3.lean:9:16: error: unknown universe 'v'
 Type
 t3.lean:14:16: error: unknown universe 'z'
-t3.lean:16:2: error: invalid namespace declaration, a namespace cannot be declared inside a section or context
+t3.lean:16:2: error: invalid namespace declaration, a namespace cannot be declared inside a section
 Type
 Type
 Type
diff --git a/tests/lua/scope.lua b/tests/lua/scope.lua
index 9a39e1bee..f60a4cfea 100644
--- a/tests/lua/scope.lua
+++ b/tests/lua/scope.lua
@@ -66,9 +66,3 @@ for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. to
 assert(get_num_coercions(env) == 6)
 print("---------")
 env = pop_scope(env)
-assert(get_num_coercions(env) == 3)
-env = pop_scope(env, "tst")
-for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
-assert(get_num_coercions(env) == 1)
-env = push_scope(env, "tst")
-assert(get_num_coercions(env) == 3)