chore(tests): remove most occurrences of 'context' command from the test suite

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 :=

tests/lean/crash.lean

@@ -1,6 +1,6 @@
 import logic
 
-context
+section
 hypothesis P : Prop.
 
 definition crash

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

tests/lean/ctxopt.lean.expected.out

@@ -1,2 +1,2 @@
 @id Prop true : Prop
-id true : Prop
+@id Prop true : Prop

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)

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

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)

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}

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

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}

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 :=
   _

tests/lean/run/466.lean

@@ -1,6 +1,6 @@
 open eq
 
-context
+section
   parameter (A : Type)
 
   definition foo (a : A) : a = a := refl a

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

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

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

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}}

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))

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),

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

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]

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

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

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

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

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) :=

tests/lean/run/localcoe.lean

@@ -1,6 +1,6 @@
 open nat
 
-context
+section
   inductive NatA :=
   | a : NatA
   | s : NatA → NatA

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)

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

tests/lean/run/one.lean

@@ -10,7 +10,7 @@ unit : one2
 
 check one2
 
-context foo
+section foo
   universe l2
   parameter A : Type.{l2}
 

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 :=

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

tests/lean/run/section3.lean

@@ -1,4 +1,4 @@
-context
+section
   parameter (A : Type)
   definition foo := A
   theorem bar {X : Type} {A : X} : foo :=

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
 

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

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) :=

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}

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]

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

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₄}

tests/lean/sec3.lean

@@ -1,4 +1,4 @@
-context
+section
   parameter A : Type
   definition tst (a : A) := a
   set_option pp.universes true

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

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

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

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

tests/lean/var.lean

@@ -1,7 +1,7 @@
 import logic
 
 
-context
+section
   variable A : Type
   parameter a : A
 end

tests/lean/var2.lean

@@ -1,7 +1,7 @@
 import logic
 
 
-context
+section
   universe l
   variable A : Type.{l}
   variable a : A