diff --git a/tests/lean/cls_err.lean b/tests/lean/cls_err.lean
index 7f5b3132d..ca62a559d 100644
--- a/tests/lean/cls_err.lean
+++ b/tests/lean/cls_err.lean
@@ -6,7 +6,7 @@ mk : A → H A
 definition foo {A : Type} [h : H A] : A :=
 H.rec (λa, a) h
 
-context
+section
   variable A : Type
   variable h : H A
   definition tst : A :=
diff --git a/tests/lean/crash.lean b/tests/lean/crash.lean
index db7e8bd4a..1130a7fe7 100644
--- a/tests/lean/crash.lean
+++ b/tests/lean/crash.lean
@@ -1,6 +1,6 @@
 import logic
 
-context
+section
 hypothesis P : Prop.
 
 definition crash
diff --git a/tests/lean/ctxopt.lean b/tests/lean/ctxopt.lean
index af96a7f26..32ac6b6c6 100644
--- a/tests/lean/ctxopt.lean
+++ b/tests/lean/ctxopt.lean
@@ -1,7 +1,7 @@
 import logic
 definition id {A : Type} (a : A) := a
 
-context
+section
   set_option pp.implicit true
   check id true
 end
diff --git a/tests/lean/ctxopt.lean.expected.out b/tests/lean/ctxopt.lean.expected.out
index d75e4dd64..2e5262270 100644
--- a/tests/lean/ctxopt.lean.expected.out
+++ b/tests/lean/ctxopt.lean.expected.out
@@ -1,2 +1,2 @@
 @id Prop true : Prop
-id true : Prop
+@id Prop true : Prop
diff --git a/tests/lean/fold.lean b/tests/lean/fold.lean
index f29e2ebba..4d88f2ea8 100644
--- a/tests/lean/fold.lean
+++ b/tests/lean/fold.lean
@@ -3,29 +3,32 @@ definition Prop := Type.{0} inductive true : Prop := intro : true inductive fals
 inductive prod (A B : Type) := mk : A → B → prod A B infixl `×`:30 := prod
 variables a b c : num
 
-context
-  notation `(` t:(foldr `,` (e r, prod.mk e r)) `)` := t
+section
+  local notation `(` t:(foldr `,` (e r, prod.mk e r)) `)` := t
   check (a, false, b, true, c)
   set_option pp.notation false
   check (a, false, b, true, c)
 end
 
-context
-  notation `(` t:(foldr `,` (e r, prod.mk r e)) `)` := t
+section
+  local notation `(` t:(foldr `,` (e r, prod.mk r e)) `)` := t
+  set_option pp.notation true
   check (a, false, b, true, c)
   set_option pp.notation false
   check (a, false, b, true, c)
 end
 
-context
-  notation `(` t:(foldl `,` (e r, prod.mk r e)) `)` := t
+section
+  local notation `(` t:(foldl `,` (e r, prod.mk r e)) `)` := t
+  set_option pp.notation true
   check (a, false, b, true, c)
   set_option pp.notation false
   check (a, false, b, true, c)
 end
 
-context
-  notation `(` t:(foldl `,` (e r, prod.mk e r)) `)` := t
+section
+  local notation `(` t:(foldl `,` (e r, prod.mk e r)) `)` := t
+  set_option pp.notation true
   check (a, false, b, true, c)
   set_option pp.notation false
   check (a, false, b, true, c)
diff --git a/tests/lean/hott/360_2.hlean b/tests/lean/hott/360_2.hlean
index 1b2f759c1..0669962f7 100644
--- a/tests/lean/hott/360_2.hlean
+++ b/tests/lean/hott/360_2.hlean
@@ -1,7 +1,7 @@
 open is_trunc
 --structure is_contr [class] (A : Type) : Type
 
-context
+section
 parameters {P : Π(A : Type), A → Type}
 
 definition my_contr {A : Type} [H : is_contr A] (a : A) : P A a := sorry
diff --git a/tests/lean/hott/443.hlean b/tests/lean/hott/443.hlean
index 61b0a2895..8ad62b67c 100644
--- a/tests/lean/hott/443.hlean
+++ b/tests/lean/hott/443.hlean
@@ -2,7 +2,7 @@ import algebra.group algebra.precategory.basic
 
 open eq sigma unit category path_algebra
 
-context
+section
   parameters {P₀ : Type} [P : precategory P₀]
 
   structure my_structure := (a : P₀) (b : P₀) (f : @hom P₀ P a b)
diff --git a/tests/lean/hott/443_b.hlean b/tests/lean/hott/443_b.hlean
index f7da25604..d78102bde 100644
--- a/tests/lean/hott/443_b.hlean
+++ b/tests/lean/hott/443_b.hlean
@@ -5,7 +5,7 @@ open eq sigma unit category path_algebra equiv
 set_option pp.implicit true
 set_option pp.universes true
 set_option pp.notation false
-context
+section
   parameters {D₀ : Type} [C : precategory D₀]
     {D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d)
       (h : hom a c) (i : hom b d), Type}
diff --git a/tests/lean/hott/apply_class_issue.hlean b/tests/lean/hott/apply_class_issue.hlean
index 1824583c3..db6a6a09d 100644
--- a/tests/lean/hott/apply_class_issue.hlean
+++ b/tests/lean/hott/apply_class_issue.hlean
@@ -1,6 +1,6 @@
 open is_trunc
 
-context
+section
 parameters {P : Π(A : Type), A → Type}
 
 definition my_contr {A : Type} [H : is_contr A] (a : A) : P A a := sorry
diff --git a/tests/lean/hott/bug_struct_level.hlean b/tests/lean/hott/bug_struct_level.hlean
index a6005466d..3cf440d69 100644
--- a/tests/lean/hott/bug_struct_level.hlean
+++ b/tests/lean/hott/bug_struct_level.hlean
@@ -2,7 +2,7 @@ import algebra.precategory.basic
 
 open category
 
-context
+section
   parameter {D₀ : Type}
   parameter (C  : precategory D₀)
   parameter (D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), Type)
@@ -22,7 +22,7 @@ context
   (ID₁       : ID₁_type)
 end
 
-context
+section
   parameter {D₀ : Type}
   parameter [C : precategory D₀]
   parameter {D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), Type}
diff --git a/tests/lean/open_tst.lean b/tests/lean/open_tst.lean
index bcf4f8ab6..548c8deb3 100644
--- a/tests/lean/open_tst.lean
+++ b/tests/lean/open_tst.lean
@@ -1,10 +1,10 @@
-context
+section
   open [notations] [coercions] nat
   check 1 + 2
   check add -- Error aliases were not created
 end
 
-context
+section
   open [declarations] [notations] nat
   variable a : nat
   check a + a
@@ -12,7 +12,7 @@ context
   check a + 1 -- Error coercion from num to nat was not loaded
 end
 
-context
+section
   open - [classes] nat
   variable a : nat
   check a + a
@@ -22,7 +22,7 @@ context
   _ -- Error inhabited instances was not loaded
 end
 
-context
+section
   open - [classes] [decls] nat
   variable a : nat
   check a + a
@@ -32,7 +32,7 @@ context
   _ -- Error inhabited instances was not loaded
 end
 
-context
+section
   open [classes] nat
   definition foo3 : inhabited nat :=
   _
diff --git a/tests/lean/run/466.lean b/tests/lean/run/466.lean
index 4f8f75463..6716d61fc 100644
--- a/tests/lean/run/466.lean
+++ b/tests/lean/run/466.lean
@@ -1,6 +1,6 @@
 open eq
 
-context
+section
   parameter (A : Type)
 
   definition foo (a : A) : a = a := refl a
diff --git a/tests/lean/run/alg_rw.lean b/tests/lean/run/alg_rw.lean
index acb775d63..d911b3e61 100644
--- a/tests/lean/run/alg_rw.lean
+++ b/tests/lean/run/alg_rw.lean
@@ -1,7 +1,7 @@
 import algebra.group
 open algebra
 
-context
+section
   variable {A : Type}
   variable [s : comm_monoid A]
   include s
@@ -13,7 +13,7 @@ end
 definition one [reducible] (A : Type) [s : has_one A] : A :=
 !has_one.one
 
-context
+section
   variable {A : Type}
   variable [s : comm_group A]
   include s
diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean
index 0ecdef98a..c26351671 100644
--- a/tests/lean/run/algebra1.lean
+++ b/tests/lean/run/algebra1.lean
@@ -3,13 +3,13 @@ import logic
 namespace experiment
 definition Type1 := Type.{1}
 
-context
+section
   variable {A  : Type}
   variable f   : A → A → A
   variable one : A
   variable inv : A → A
-  infixl `*`     := f
-  postfix `^-1`:100 := inv
+  local infixl `*`     := f
+  local postfix `^-1`:100 := inv
   definition is_assoc := ∀ a b c, (a*b)*c = a*b*c
   definition is_id    := ∀ a, a*one = a
   definition is_inv   := ∀ a, a*a^-1 = one
diff --git a/tests/lean/run/alias3.lean b/tests/lean/run/alias3.lean
index b5e7f914b..e1e4b495c 100644
--- a/tests/lean/run/alias3.lean
+++ b/tests/lean/run/alias3.lean
@@ -1,8 +1,8 @@
 import logic
 
 namespace N1
-  context
-    context
+  section
+    section
       parameter A : Type
       definition foo (a : A) : Prop := true
       check foo
@@ -14,7 +14,7 @@ end N1
 check N1.foo
 
 namespace N2
-  context
+  section
     parameter A : Type
     inductive list : Type :=
     | nil {} : list
diff --git a/tests/lean/run/basic.lean b/tests/lean/run/basic.lean
index f54dfcb7d..ead66d56a 100644
--- a/tests/lean/run/basic.lean
+++ b/tests/lean/run/basic.lean
@@ -37,9 +37,9 @@ infix `=`:50 := eq
 
 check eq.{1}
 
-context
-  universe l
-  universe u
+section
+  universe variable l
+  universe variable u
   variable {T1 : Type.{l}}
   variable {T2 : Type.{l}}
   variable {T3 : Type.{u}}
diff --git a/tests/lean/run/cody1.lean b/tests/lean/run/cody1.lean
index 7e4c3d136..98d09f0f8 100644
--- a/tests/lean/run/cody1.lean
+++ b/tests/lean/run/cody1.lean
@@ -2,7 +2,7 @@ import logic
 
 definition subsets (P : Type) := P → Prop.
 
-context
+section
 
 hypothesis A : Type.
 
@@ -14,7 +14,7 @@ hypothesis retract {P : subsets A} {a : A} : r (i P) a = P a.
 
 definition delta (a:A) : Prop := ¬ (r a a).
 
-notation `δ` := delta.
+local notation `δ` := delta.
 
 -- Crashes unifier!
 theorem false_aux : ¬ (δ (i delta))
diff --git a/tests/lean/run/cody2.lean b/tests/lean/run/cody2.lean
index d18ac0c84..86cb26269 100644
--- a/tests/lean/run/cody2.lean
+++ b/tests/lean/run/cody2.lean
@@ -2,7 +2,7 @@ import logic
 open eq
 definition subsets (P : Type) := P → Prop.
 
-context
+section
 
 hypothesis A : Type.
 
@@ -14,7 +14,7 @@ hypothesis retract {P : subsets A} {a : A} : r (i P) a = P a.
 
 definition delta (a:A) : Prop := ¬ (r a a).
 
-notation `δ` := delta.
+local notation `δ` := delta.
 
 theorem delta_aux : ¬ (δ (i delta))
          := assume H : δ (i delta),
diff --git a/tests/lean/run/def_tac.lean b/tests/lean/run/def_tac.lean
index 2f4f7ec82..360d31d70 100644
--- a/tests/lean/run/def_tac.lean
+++ b/tests/lean/run/def_tac.lean
@@ -1,4 +1,4 @@
-context
+section
   open tactic
   definition cases_refl (e : expr) : tactic :=
   cases e expr_list.nil; apply rfl
diff --git a/tests/lean/run/eq20.lean b/tests/lean/run/eq20.lean
index a953a9d98..390eff227 100644
--- a/tests/lean/run/eq20.lean
+++ b/tests/lean/run/eq20.lean
@@ -1,7 +1,7 @@
 import data.list
 open nat list
 
-context
+section
   parameter {A : Type}
   parameter (p : A → Prop)
   parameter [H : decidable_pred p]
diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean
index 3c4dc3b9f..02323593b 100644
--- a/tests/lean/run/group.lean
+++ b/tests/lean/run/group.lean
@@ -1,12 +1,12 @@
 import logic
 
-context
+section
   variable {A  : Type}
   variable f   : A → A → A
   variable one : A
   variable inv : A → A
-  infixl `*`   := f
-  postfix `^-1`:100 := inv
+  local infixl `*`   := f
+  local postfix `^-1`:100 := inv
   definition is_assoc := ∀ a b c, (a*b)*c = a*b*c
   definition is_id    := ∀ a, a*one = a
   definition is_inv   := ∀ a, a*a^-1 = one
diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean
index f7ff60a4e..a609eeb8a 100644
--- a/tests/lean/run/group2.lean
+++ b/tests/lean/run/group2.lean
@@ -1,12 +1,12 @@
 import logic
 
-context
+section
   variable {A  : Type}
   variable f   : A → A → A
   variable one : A
   variable inv : A → A
-  infixl `*`     := f
-  postfix `^-1`:100 := inv
+  local infixl `*`     := f
+  local postfix `^-1`:100 := inv
   definition is_assoc := ∀ a b c, (a*b)*c = a*b*c
   definition is_id    := ∀ a, a*one = a
   definition is_inv   := ∀ a, a*a^-1 = one
diff --git a/tests/lean/run/group3.lean b/tests/lean/run/group3.lean
index ada7477fd..d8c3828aa 100644
--- a/tests/lean/run/group3.lean
+++ b/tests/lean/run/group3.lean
@@ -43,7 +43,7 @@ section
   variables {A : Type} [s : semigroup A]
   variables a b c : A
   definition mul := semigroup.rec (λmul assoc, mul) s a b
-  context
+  section
     infixl `*` := mul
     definition assoc : (a * b) * c = a * (b * c) :=
       semigroup.rec (λmul assoc, assoc) s a b c
@@ -111,7 +111,7 @@ namespace monoid
   variables {A : Type} [s : monoid A]
   variables a b c : A
   include s
-  context
+  section
   definition mul := monoid.rec (λmul one assoc right_id left_id, mul) s a b
   definition one := monoid.rec (λmul one assoc right_id left_id, one) s
   infixl `*` := mul
diff --git a/tests/lean/run/imp3.lean b/tests/lean/run/imp3.lean
index 9fc586ce9..b82d21cf3 100644
--- a/tests/lean/run/imp3.lean
+++ b/tests/lean/run/imp3.lean
@@ -3,7 +3,7 @@ structure is_equiv [class] {A B : Type} (f : A → B) :=
 
 check @is_equiv.inv
 namespace is_equiv
-context
+section
    parameters A B : Type
    parameter  f : A → B
    parameter  c : is_equiv f
diff --git a/tests/lean/run/indbug2.lean b/tests/lean/run/indbug2.lean
index 1dce9422f..3ba77c9b1 100644
--- a/tests/lean/run/indbug2.lean
+++ b/tests/lean/run/indbug2.lean
@@ -1,6 +1,6 @@
 set_option pp.implicit true
 set_option pp.universes true
-context
+section
 parameter {A : Type}
 definition foo : A → A → Type := (λ x y, Type)
 inductive bar {a b : A} (f : foo a b) :=
diff --git a/tests/lean/run/localcoe.lean b/tests/lean/run/localcoe.lean
index 9866919c1..e8f8a7514 100644
--- a/tests/lean/run/localcoe.lean
+++ b/tests/lean/run/localcoe.lean
@@ -1,6 +1,6 @@
 open nat
 
-context
+section
   inductive NatA :=
   | a : NatA
   | s : NatA → NatA
diff --git a/tests/lean/run/match3.lean b/tests/lean/run/match3.lean
index 1f903778e..c94bcc047 100644
--- a/tests/lean/run/match3.lean
+++ b/tests/lean/run/match3.lean
@@ -21,7 +21,7 @@ protected theorem dec_eq : ∀ x y : nat, decidable (x = y)
   | inr H := inr (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H))
   end
 
-context
+section
   open list
   parameter {A : Type}
   parameter (p : A → Prop)
diff --git a/tests/lean/run/n4.lean b/tests/lean/run/n4.lean
index 3ed24fafa..6e2e9fb04 100644
--- a/tests/lean/run/n4.lean
+++ b/tests/lean/run/n4.lean
@@ -1,16 +1,16 @@
 prelude
 definition Prop : Type.{1} := Type.{0}
-context
+section
   variable N : Type.{1}
   variables a b c : N
   variable and : Prop → Prop → Prop
-  infixr `∧`:35 := and
+  local infixr `∧`:35 := and
   variable le : N → N → Prop
   variable lt : N → N → Prop
   precedence `≤`:50
   precedence `<`:50
-  infixl ≤ := le
-  infixl < := lt
+  local infixl ≤ := le
+  local infixl < := lt
   check a ≤ b
   definition T : Prop := a ≤ b
   check T
diff --git a/tests/lean/run/one.lean b/tests/lean/run/one.lean
index fbc8a71ca..177d9dc3c 100644
--- a/tests/lean/run/one.lean
+++ b/tests/lean/run/one.lean
@@ -10,7 +10,7 @@ unit : one2
 
 check one2
 
-context foo
+section foo
   universe l2
   parameter A : Type.{l2}
 
diff --git a/tests/lean/run/record2.lean b/tests/lean/run/record2.lean
index 7636e65f6..34a47978d 100644
--- a/tests/lean/run/record2.lean
+++ b/tests/lean/run/record2.lean
@@ -2,10 +2,10 @@ import logic data.unit
 
 set_option pp.universes true
 
-context
+section
   parameter (A : Type)
 
-  context
+  section
     parameter (B : Type)
 
     structure point :=
diff --git a/tests/lean/run/sec_var.lean b/tests/lean/run/sec_var.lean
index a6a042064..a004a59ff 100644
--- a/tests/lean/run/sec_var.lean
+++ b/tests/lean/run/sec_var.lean
@@ -1,6 +1,6 @@
 import logic
 
-context
+section
   parameter A : Type
   definition foo : ∀ ⦃ a b : A ⦄, a = b → a = b :=
   take a b H, H
diff --git a/tests/lean/run/section3.lean b/tests/lean/run/section3.lean
index 3a12c83b5..0623525d2 100644
--- a/tests/lean/run/section3.lean
+++ b/tests/lean/run/section3.lean
@@ -1,4 +1,4 @@
-context
+section
   parameter (A : Type)
   definition foo := A
   theorem bar {X : Type} {A : X} : foo :=
diff --git a/tests/lean/run/section4.lean b/tests/lean/run/section4.lean
index 72b2b1a6c..f70eb4a3b 100644
--- a/tests/lean/run/section4.lean
+++ b/tests/lean/run/section4.lean
@@ -3,13 +3,13 @@ import logic
   set_option pp.universes true
   set_option pp.implicit true
 
-context
+section
   universe k
   parameter A : Type
 
   context
-    universe l
-    universe u
+    universe variable l
+    universe variable u
     parameter B : Type
     definition foo (a : A) (b : B) := b
 
diff --git a/tests/lean/run/simple.lean b/tests/lean/run/simple.lean
index e2ae78513..623851345 100644
--- a/tests/lean/run/simple.lean
+++ b/tests/lean/run/simple.lean
@@ -1,6 +1,6 @@
 prelude
 definition Prop : Type.{1} := Type.{0}
-context
+section
   parameter A : Type
 
   definition eq (a b : A) : Prop
diff --git a/tests/lean/run/struct_bug1.lean b/tests/lean/run/struct_bug1.lean
index 304ef761c..b2316a988 100644
--- a/tests/lean/run/struct_bug1.lean
+++ b/tests/lean/run/struct_bug1.lean
@@ -3,7 +3,7 @@ variable (A : Type)
 structure foo (a : A) :=
 (eqpr : a = a)
 
-context
+section
  parameter (B : Type)
 
  structure foo2 (b : B) :=
diff --git a/tests/lean/run/structure_test.lean b/tests/lean/run/structure_test.lean
index fb2acec86..d2ea0389b 100644
--- a/tests/lean/run/structure_test.lean
+++ b/tests/lean/run/structure_test.lean
@@ -27,7 +27,7 @@ section
   check point3d_color.to_point
 end
 
-context
+section
   universe l
   parameters A : Type.{l}
   parameters B : Type.{l}
diff --git a/tests/lean/run/t11.lean b/tests/lean/run/t11.lean
index 80e405181..cd0596e5e 100644
--- a/tests/lean/run/t11.lean
+++ b/tests/lean/run/t11.lean
@@ -2,7 +2,7 @@ constant A : Type.{1}
 constants a b c : A
 constant f : A → A → A
 check f a b
-context
+section
   parameters A B : Type
   parameters {C D : Type}
   parameters [e d : A]
diff --git a/tests/lean/run/univ1.lean b/tests/lean/run/univ1.lean
index 66f4d4592..62c3dfca7 100644
--- a/tests/lean/run/univ1.lean
+++ b/tests/lean/run/univ1.lean
@@ -19,7 +19,7 @@ end S2
 
 
 namespace S3
-context
+section
   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 fb1d21ee2..40abfdb08 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
-context
+section
   universes l₁ l₂ l₃ l₄
   parameter C : Category.{l₁ l₂}
   parameter f : Category.{l₁ l₂} → Category.{l₃ l₄}
diff --git a/tests/lean/sec3.lean b/tests/lean/sec3.lean
index ad8f9f749..b5920481a 100644
--- a/tests/lean/sec3.lean
+++ b/tests/lean/sec3.lean
@@ -1,4 +1,4 @@
-context
+section
   parameter A : Type
   definition tst (a : A) := a
   set_option pp.universes true
diff --git a/tests/lean/t14.lean b/tests/lean/t14.lean
index fc566b95f..448448b2c 100644
--- a/tests/lean/t14.lean
+++ b/tests/lean/t14.lean
@@ -5,25 +5,25 @@ prelude namespace foo
   constant c : A
 end foo
 
-context
+section
   open foo (renaming a->b x->y) (hiding c)
   check b
   check y
   check c -- Error
 end
 
-context
+section
   open foo (a x)
   check a
   check x
   check c -- Error
 end
 
-context
+section
   open foo (a x) (hiding c) -- Error
 end
 
-context
+section
   open foo
   check a
   check c
@@ -35,18 +35,18 @@ namespace foo
   infix `*`:75 := f
 end foo
 
-context
+section
   open foo
   check a * c
 end
 
-context
+section
   open [notations] foo -- use only the notation
   check foo.a * foo.c
   check a * c -- Error
 end
 
-context
+section
   open [decls] foo -- use only the declarations
   check f a c
   check a*c -- Error
diff --git a/tests/lean/t3.lean b/tests/lean/t3.lean
index 6f149b856..830f4323f 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
-context
-  universe z        -- Remark: this is a local universe
+section
+  universe variable z -- Remark: this is a local universe
   print raw Type.{z}
 end
 print raw Type.{z}  -- Error: local universe 'z' is gone
-context
-  namespace foo -- Error: we cannot create a namespace inside a context
+section
+  namespace foo -- Error: we cannot create a namespace inside a section
 end
 namespace tst
   print raw Type.{v} -- Remark: alias 'v' is available again
diff --git a/tests/lean/t4.lean b/tests/lean/t4.lean
index 12ebf8ed6..5f22069d1 100644
--- a/tests/lean/t4.lean
+++ b/tests/lean/t4.lean
@@ -13,7 +13,7 @@ constant f (a b : N) : N
 constant len.{l} (A : Type.{l}) (n : N) (v : vec.{l} A n) : N
 check f
 check len.{1}
-context
+section
    parameter A  : Type
    parameter B  : Prop
    hypothesis H : B
diff --git a/tests/lean/t7.lean b/tests/lean/t7.lean
index 7e25aae2a..3704d002b 100644
--- a/tests/lean/t7.lean
+++ b/tests/lean/t7.lean
@@ -1,6 +1,6 @@
 prelude definition Prop : Type.{1} := Type.{0}
 constant and : Prop → Prop → Prop
-context
+section
   parameter {A : Type}  -- Mark A as implicit parameter
   parameter   R : A → A → Prop
   parameter   B : Type
diff --git a/tests/lean/var.lean b/tests/lean/var.lean
index 1089a8bdd..e8109d8c4 100644
--- a/tests/lean/var.lean
+++ b/tests/lean/var.lean
@@ -1,7 +1,7 @@
 import logic
 
 
-context
+section
   variable A : Type
   parameter a : A
 end
diff --git a/tests/lean/var2.lean b/tests/lean/var2.lean
index 836f1151e..6007f7c7a 100644
--- a/tests/lean/var2.lean
+++ b/tests/lean/var2.lean
@@ -1,7 +1,7 @@
 import logic
 
 
-context
+section
   universe l
   variable A : Type.{l}
   variable a : A