diff --git a/hott/init/axioms/funext_varieties.hlean b/hott/init/axioms/funext_varieties.hlean
index 16396a104..c1a8e1faa 100644
--- a/hott/init/axioms/funext_varieties.hlean
+++ b/hott/init/axioms/funext_varieties.hlean
@@ -50,8 +50,8 @@ definition weak_funext_of_naive_funext : naive_funext → weak_funext :=
   funext, the space of "pointwise homotopies" has the same universal property as
   the space of paths. -/
 
-context
-  universes l k
+section
+  universe variables l k
   parameters [wf : weak_funext.{l k}] {A : Type.{l}} {B : A → Type.{k}} (f : Π x, B x)
 
   definition is_contr_sigma_homotopy [instance] : is_contr (Σ (g : Π x, B x), f ∼ g) :=
@@ -86,7 +86,6 @@ context
   local attribute homotopy_ind [reducible]
   definition homotopy_ind_comp : homotopy_ind f (homotopy.refl f) = d :=
     (@hprop_eq_of_is_contr _ _ _ _ !center_eq idp)⁻¹ ▹ idp
-
 end
 
 -- Now the proof is fairly easy; we can just use the same induction principle on both sides.
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 07d4c7e9c..4500f94b9 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1174,7 +1174,7 @@ name parser::check_constant_next(char const * msg) {
     name id = check_id_next(msg);
     expr e  = id_to_expr(id, p);
 
-    if (in_context(m_env) && is_as_atomic(e)) {
+    if ((in_section(m_env) || 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/tests/lean/bad_coercions.lean b/tests/lean/bad_coercions.lean
deleted file mode 100644
index d724b3603..000000000
--- a/tests/lean/bad_coercions.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-open nat
-
-constant list.{l} : Type.{l} → Type.{l}
-constant vector.{l} : Type.{l} → nat → Type.{l}
-constant nil (A : Type) : list A
-
-set_option pp.coercions true
-context
-  parameter A : Type
-  parameter n : nat
-
-  definition foo2 [coercion] (v : vector A n) : list A :=
-  nil A
-
-  definition foo (v : vector A n) : list A :=
-  nil A
-
-  attribute foo [coercion]
-end
diff --git a/tests/lean/bad_coercions.lean.expected.out b/tests/lean/bad_coercions.lean.expected.out
deleted file mode 100644
index 04ed19d55..000000000
--- a/tests/lean/bad_coercions.lean.expected.out
+++ /dev/null
@@ -1,2 +0,0 @@
-bad_coercions.lean:12:18: error: invalid '[coercion]' attribute, (non local) coercions cannot be defined in contexts
-bad_coercions.lean:18:16: error: invalid '[coercion]' attribute, (non local) coercions cannot be defined in contexts
diff --git a/tests/lean/run/class_bug1.lean b/tests/lean/run/class_bug1.lean
index d085d603e..912bbdb50 100644
--- a/tests/lean/run/class_bug1.lean
+++ b/tests/lean/run/class_bug1.lean
@@ -11,7 +11,7 @@ mk : Π (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
 attribute category [class]
 
 namespace category
-context sec_cat
+section sec_cat
   parameter A : Type
   inductive foo :=
   mk : A → foo
@@ -20,7 +20,7 @@ context sec_cat
   parameters {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor}
   definition compose := category.rec (λ comp id assoc idr idl, comp) Cat
   definition id := category.rec (λ comp id assoc idr idl, id) Cat
-  infixr ∘ := compose
+  local infixr ∘ := compose
   inductive is_section {A B : ob} (f : mor A B) : Type :=
   mk : ∀g, g ∘ f = id → is_section f
 end sec_cat