diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 517f778921..18d2637bad 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -121,7 +121,7 @@ static void redeclare_aliases(parser & p,
                               list<pair<name, level>> old_level_entries,
                               list<pair<name, expr>> old_entries) {
     environment const & env = p.env();
-    if (!in_section_or_context(env))
+    if (!in_context(env))
         return;
     list<pair<name, expr>> new_entries = p.get_local_entries();
     buffer<pair<name, expr>> to_redeclare;
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index e16f9a7c31..047d6183bb 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -25,7 +25,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 static environment declare_universe(parser & p, environment env, name const & n, bool local) {
-    if (in_section_or_context(env) || local) {
+    if (in_context(env) || local) {
         p.add_local_level(n, mk_param_univ(n));
     } else {
         name const & ns = get_namespace(env);
@@ -112,7 +112,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_section_or_context(p);
+            check_in_context(p);
             check_parameter_type(p, n, type, pos);
         }
         if (p.get_local(n))
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index aa0978bd1f..0681e87d47 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -49,7 +49,7 @@ static unsigned parse_precedence(parser & p, char const * msg) {
 
 LEAN_THREAD_VALUE(bool, g_allow_local, false);
 
-static void check_notation_expr(parser & p, expr const & e, pos_info const & pos) {
+static void check_notation_expr(expr const & e, pos_info const & pos) {
     if (!g_allow_local && (has_local(e) || has_param_univ(e)))
         throw parser_error("invalid notation declaration, contains reference to local variables", pos);
 }
@@ -89,7 +89,7 @@ static pair<notation_entry, optional<token_entry>> parse_mixfix_notation(parser
     p.check_token_next(get_assign_tk(), "invalid notation declaration, ':=' expected");
     auto f_pos = p.pos();
     expr f     = p.parse_expr();
-    check_notation_expr(p, f, f_pos);
+    check_notation_expr(f, f_pos);
     char const * tks = tk.c_str();
     switch (k) {
     case mixfix_kind::infixl:
@@ -145,7 +145,7 @@ static expr parse_notation_expr(parser & p, buffer<expr> const & locals) {
     auto pos = p.pos();
     expr r = p.parse_expr();
     r = abstract(r, locals.size(), locals.data());
-    check_notation_expr(p, r, pos);
+    check_notation_expr(r, pos);
     return r;
 }
 
@@ -273,7 +273,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, buffer<toke
         p.check_token_next(get_assign_tk(), "invalid numeral notation, `:=` expected");
         auto e_pos = p.pos();
         expr e     = p.parse_expr();
-        check_notation_expr(p, e, e_pos);
+        check_notation_expr(e, e_pos);
         return notation_entry(num, e, overload);
     } else if (p.curr_is_identifier()) {
         parse_notation_local(p, locals);
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 72b4cfd158..57f0992376 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1074,7 +1074,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_or_context(m_env) && is_as_atomic(e)) {
+    if (in_context(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/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 32ee2f58c9..3829682c24 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -114,9 +114,9 @@ struct structure_cmd_fn {
         }
     }
 
-    /** \brief Include in m_level_names any section level referenced m_type and m_fields */
-    void include_section_levels() {
-        if (!in_section_or_context(m_env))
+    /** \brief Include in m_level_names any local level referenced m_type and m_fields */
+    void include_local_levels() {
+        if (!in_context(m_env))
             return;
         name_set all_lvl_params;
         all_lvl_params = collect_univ_params(m_type);
@@ -144,11 +144,11 @@ struct structure_cmd_fn {
         collect_locals(tmp, ls);
     }
 
-    /** \brief Include the used section parameters as additional arguments.
+    /** \brief Include the used parameters as additional arguments.
         The section parameters are stored in section_params
     */
     void abstract_section_locals(buffer<expr> & section_params) {
-        if (!in_section_or_context(m_env))
+        if (!in_context(m_env))
             return;
         expr_struct_set section_locals;
         collect_section_locals(section_locals);
@@ -265,7 +265,7 @@ struct structure_cmd_fn {
         m_p.check_token_next(get_dcolon_tk(), "invalid 'structure', '::' expected");
         m_p.parse_binders(m_fields, m_nentries);
         m_type = Pi(m_params, m_type, m_p);
-        include_section_levels();
+        include_local_levels();
         buffer<expr> section_params;
         abstract_section_locals(section_params);
         elaborate_type();
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 63cb957ddc..0f54801960 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -33,9 +33,9 @@ void check_atomic(name const & n) {
         throw exception(sstream() << "invalid declaration name '" << n << "', identifier must be atomic");
 }
 
-void check_in_section_or_context(parser const & p) {
-    if (!in_section_or_context(p.env()))
-        throw exception(sstream() << "invalid command, it must be used in a section");
+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");
 }
 bool is_root_namespace(name const & n) {
     return n == get_root_tk();
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index 0fdbd9cc0e..591a91cdc5 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -19,7 +19,7 @@ typedef std::unique_ptr<type_checker> type_checker_ptr;
 bool parse_persistent(parser & p, bool & persistent);
 
 void check_atomic(name const & n);
-void check_in_section_or_context(parser const & p);
+void check_in_context(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/tests/lean/crash.lean b/tests/lean/crash.lean
index e8b4601729..db7e8bd4ad 100644
--- a/tests/lean/crash.lean
+++ b/tests/lean/crash.lean
@@ -1,6 +1,6 @@
 import logic
 
-section
+context
 hypothesis P : Prop.
 
 definition crash
@@ -9,4 +9,4 @@ definition crash
             from H,
             _.
 
-end
\ No newline at end of file
+end
diff --git a/tests/lean/interactive/sec_info_bug.input b/tests/lean/interactive/sec_info_bug.input
index e32704304f..c56e417de4 100644
--- a/tests/lean/interactive/sec_info_bug.input
+++ b/tests/lean/interactive/sec_info_bug.input
@@ -3,7 +3,7 @@ SYNC 10
 import logic
 constant category : Type -> Type
 namespace category
-  section
+  context
   parameters {ob : Type} {C : category ob}
   variables {a b c d : ob}
   definition hom : ob → ob → Type := let aux := C in sorry
diff --git a/tests/lean/run/basic.lean b/tests/lean/run/basic.lean
index 09bde74db8..5f9b4cc230 100644
--- a/tests/lean/run/basic.lean
+++ b/tests/lean/run/basic.lean
@@ -36,7 +36,7 @@ infix `=`:50 := eq
 
 check eq.{1}
 
-section
+context
   universe l
   universe u
   variable {T1 : Type.{l}}
diff --git a/tests/lean/run/univ1.lean b/tests/lean/run/univ1.lean
index ce3b416464..e979f2f45e 100644
--- a/tests/lean/run/univ1.lean
+++ b/tests/lean/run/univ1.lean
@@ -19,7 +19,7 @@ end S2
 
 
 namespace S3
-section
+context
   hypothesis I : Type
   definition F (X : Type) : Type := (X → Prop) → Prop
   hypothesis unfold : I → F I
diff --git a/tests/lean/run/univs.lean b/tests/lean/run/univs.lean
index 40abfdb08f..fb1d21ee24 100644
--- a/tests/lean/run/univs.lean
+++ b/tests/lean/run/univs.lean
@@ -1,7 +1,7 @@
 import algebra.category.basic
 
 set_option pp.universes true
-section
+context
   universes l₁ l₂ l₃ l₄
   parameter C : Category.{l₁ l₂}
   parameter f : Category.{l₁ l₂} → Category.{l₃ l₄}
diff --git a/tests/lean/t3.lean b/tests/lean/t3.lean
index 0b67420925..6f149b8561 100644
--- a/tests/lean/t3.lean
+++ b/tests/lean/t3.lean
@@ -7,13 +7,13 @@ namespace tst
 end tst
 print raw Type.{tst.v}
 print raw Type.{v}  -- Error: alias 'v' is not available anymore
-section
+context
   universe z        -- Remark: this is a local universe
   print raw Type.{z}
 end
 print raw Type.{z}  -- Error: local universe 'z' is gone
-section
-  namespace foo -- Error: we cannot create a namespace inside a section
+context
+  namespace foo -- Error: we cannot create a namespace inside a context
 end
 namespace tst
   print raw Type.{v} -- Remark: alias 'v' is available again