From e51c4ad2e95c1598d0b4d3e5f8d84b9ee3165c8d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Sep 2014 16:00:38 -0700
Subject: [PATCH] feat(frontends/lean): rename 'using' command to 'open'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 doc/lean/calc.org                             |  4 +-
 doc/lean/tutorial.org                         | 40 +++++++++----------
 library/data/bool.lean                        |  2 +-
 library/data/int/basic.lean                   | 17 +++-----
 library/data/int/order.lean                   |  8 ++--
 library/data/list/basic.lean                  |  6 +--
 library/data/nat/basic.lean                   |  8 ++--
 library/data/nat/div.lean                     |  6 +--
 library/data/nat/order.lean                   |  6 +--
 library/data/nat/sub.lean                     |  6 +--
 library/data/option.lean                      |  2 +-
 library/data/prod.lean                        |  2 +-
 library/data/quotient/aux.lean                |  4 +-
 library/data/quotient/basic.lean              |  4 +-
 library/data/quotient/classical.lean          |  2 +-
 library/data/set.lean                         |  2 +-
 library/data/sigma.lean                       |  2 +-
 library/data/string.lean                      |  2 +-
 library/data/subtype.lean                     |  2 +-
 library/data/sum.lean                         |  2 +-
 library/data/unit.lean                        |  2 +-
 library/hott/fibrant.lean                     |  4 +-
 library/hott/path.lean                        |  4 +-
 library/logic/axioms/classical.lean           |  4 +-
 library/logic/axioms/examples/diaconescu.lean |  2 +-
 library/logic/axioms/funext.lean              |  2 +-
 library/logic/axioms/hilbert.lean             |  2 +-
 library/logic/axioms/piext.lean               |  2 +-
 library/logic/axioms/prop_decidable.lean      |  2 +-
 library/logic/classes/nonempty.lean           |  2 +-
 library/logic/core/cast.lean                  |  2 +-
 library/logic/core/eq.lean                    |  2 +-
 .../logic/core/examples/instances_test.lean   |  9 ++---
 library/logic/core/identities.lean            |  2 +-
 library/logic/core/if.lean                    |  2 +-
 library/logic/core/instances.lean             |  2 +-
 library/logic/core/quantifiers.lean           |  2 +-
 library/struc/binary.lean                     |  3 +-
 library/struc/wf.lean                         |  2 +-
 library/tools/fake_simplifier.lean            |  2 +-
 library/tools/helper_tactics.lean             |  2 +-
 library/tools/tactic.lean                     |  4 +-
 src/emacs/lean-syntax.el                      | 13 +++---
 src/frontends/lean/builtin_cmds.cpp           | 24 +++++------
 src/frontends/lean/token_table.cpp            |  4 +-
 tests/lean/alias.lean                         | 13 +++---
 tests/lean/choice_expl.lean                   |  2 +-
 tests/lean/empty.lean                         |  2 +-
 tests/lean/empty_thm.lean                     |  2 +-
 tests/lean/have1.lean                         |  2 +-
 tests/lean/interactive/class_bug.lean         |  2 +-
 tests/lean/let3.lean                          |  2 +-
 tests/lean/let4.lean                          |  4 +-
 tests/lean/num.lean                           |  2 +-
 tests/lean/protected.lean                     |  2 +-
 tests/lean/run/algebra1.lean                  |  6 +--
 tests/lean/run/alias1.lean                    |  6 +--
 tests/lean/run/alias2.lean                    |  5 +--
 tests/lean/run/booltst.lean                   |  4 +-
 tests/lean/run/calc.lean                      |  2 +-
 tests/lean/run/choice_ctx.lean                |  5 +--
 tests/lean/run/class1.lean                    |  2 +-
 tests/lean/run/class2.lean                    |  2 +-
 tests/lean/run/class3.lean                    |  2 +-
 tests/lean/run/class5.lean                    | 16 ++++----
 tests/lean/run/class6.lean                    |  2 +-
 tests/lean/run/class7.lean                    |  2 +-
 tests/lean/run/class8.lean                    |  4 +-
 tests/lean/run/class_coe.lean                 |  2 +-
 tests/lean/run/coercion_bug.lean              |  2 +-
 tests/lean/run/coercion_bug2.lean             |  2 +-
 tests/lean/run/congr_imp_bug.lean             |  2 +-
 tests/lean/run/decidable.lean                 |  2 +-
 tests/lean/run/e10.lean                       |  9 ++---
 tests/lean/run/e11.lean                       | 14 +++----
 tests/lean/run/e12.lean                       | 26 ++++++------
 tests/lean/run/e13.lean                       |  9 ++---
 tests/lean/run/e6.lean                        |  9 ++---
 tests/lean/run/e7.lean                        |  9 ++---
 tests/lean/run/e8.lean                        | 14 +++----
 tests/lean/run/e9.lean                        | 11 +++--
 tests/lean/run/elab_bug1.lean                 |  4 +-
 tests/lean/run/elim.lean                      |  2 +-
 tests/lean/run/elim2.lean                     |  2 +-
 tests/lean/run/full.lean                      |  4 +-
 tests/lean/run/fun.lean                       |  2 +-
 tests/lean/run/goal.lean                      |  4 +-
 tests/lean/run/group.lean                     |  2 +-
 tests/lean/run/group2.lean                    |  2 +-
 tests/lean/run/have5.lean                     |  4 +-
 tests/lean/run/is_nil.lean                    |  2 +-
 tests/lean/run/list_elab1.lean                |  2 +-
 tests/lean/run/local_using.lean               |  6 +--
 tests/lean/run/match1.lean                    |  2 +-
 tests/lean/run/match2.lean                    |  2 +-
 tests/lean/run/nat_bug.lean                   |  2 +-
 tests/lean/run/nat_bug2.lean                  |  2 +-
 tests/lean/run/nat_bug3.lean                  |  2 +-
 tests/lean/run/nat_bug4.lean                  |  2 +-
 tests/lean/run/nat_bug5.lean                  |  2 +-
 tests/lean/run/nat_bug6.lean                  |  2 +-
 tests/lean/run/not_bug1.lean                  |  2 +-
 tests/lean/run/ns.lean                        |  4 +-
 tests/lean/run/ns1.lean                       |  4 +-
 tests/lean/run/occurs_check_bug1.lean         |  4 +-
 tests/lean/run/over2.lean                     |  6 +--
 tests/lean/run/over_subst.lean                |  4 +-
 tests/lean/run/ptst.lean                      |  2 +-
 tests/lean/run/rel.lean                       |  2 +-
 tests/lean/run/root.lean                      |  2 +-
 tests/lean/run/section1.lean                  |  4 +-
 tests/lean/run/set.lean                       |  4 +-
 tests/lean/run/set2.lean                      |  4 +-
 tests/lean/run/sum_bug.lean                   |  2 +-
 tests/lean/run/t8.lean                        |  4 +-
 tests/lean/run/tactic1.lean                   |  2 +-
 tests/lean/run/tactic10.lean                  |  2 +-
 tests/lean/run/tactic11.lean                  |  2 +-
 tests/lean/run/tactic12.lean                  |  2 +-
 tests/lean/run/tactic13.lean                  |  2 +-
 tests/lean/run/tactic14.lean                  |  2 +-
 tests/lean/run/tactic15.lean                  |  2 +-
 tests/lean/run/tactic16.lean                  |  2 +-
 tests/lean/run/tactic17.lean                  |  2 +-
 tests/lean/run/tactic18.lean                  |  2 +-
 tests/lean/run/tactic19.lean                  |  2 +-
 tests/lean/run/tactic2.lean                   |  4 +-
 tests/lean/run/tactic20.lean                  |  2 +-
 tests/lean/run/tactic21.lean                  |  2 +-
 tests/lean/run/tactic22.lean                  |  2 +-
 tests/lean/run/tactic23.lean                  |  4 +-
 tests/lean/run/tactic24.lean                  |  2 +-
 tests/lean/run/tactic25.lean                  |  2 +-
 tests/lean/run/tactic26.lean                  |  2 +-
 tests/lean/run/tactic27.lean                  |  2 +-
 tests/lean/run/tactic28.lean                  |  2 +-
 tests/lean/run/tactic29.lean                  |  4 +-
 tests/lean/run/tactic3.lean                   |  4 +-
 tests/lean/run/tactic30.lean                  |  4 +-
 tests/lean/run/tactic4.lean                   |  2 +-
 tests/lean/run/tactic5.lean                   |  4 +-
 tests/lean/run/tactic6.lean                   |  2 +-
 tests/lean/run/tactic7.lean                   |  2 +-
 tests/lean/run/tactic8.lean                   |  4 +-
 tests/lean/run/tactic9.lean                   |  2 +-
 tests/lean/run/trick.lean                     |  2 +-
 tests/lean/run/univ_bug1.lean                 |  4 +-
 tests/lean/run/univ_bug2.lean                 |  4 +-
 tests/lean/show1.lean                         |  2 +-
 tests/lean/slow/list_elab2.lean               |  6 +--
 tests/lean/slow/nat_wo_hints.lean             |  6 +--
 tests/lean/slow/path_groupoids.lean           |  2 +-
 tests/lean/t14.lean                           | 14 +++----
 tests/lean/t14.lean.expected.out              |  2 +-
 tests/lean/uni_bug1.lean                      |  2 +-
 155 files changed, 312 insertions(+), 336 deletions(-)

diff --git a/doc/lean/calc.org b/doc/lean/calc.org
index c8f123aeb..782711e21 100644
--- a/doc/lean/calc.org
+++ b/doc/lean/calc.org
@@ -26,7 +26,7 @@ Here is an example
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
   variables a b c d e : nat.
   axiom Ax1 : a = b.
   axiom Ax2 : b = c + 1.
@@ -55,7 +55,7 @@ some form of transitivity. It can even combine different relations.
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
 
   theorem T2 (a b c : nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0
   := calc  a = b      : H1
diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org
index dccc0e794..c4de00b7b 100644
--- a/doc/lean/tutorial.org
+++ b/doc/lean/tutorial.org
@@ -30,7 +30,7 @@ the input value.
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
   -- defines the double function
   definition double (x : nat) := x + x
 #+END_SRC
@@ -62,7 +62,7 @@ The command =import= loads existing libraries and extensions.
 
 We say =nat.ge= is a hierarchical name comprised of two parts: =nat= and =ge=.
 
-The command =using= creates aliases based on a given prefix. The
+The command =open= creates aliases based on a given prefix. The
 command also imports notation, hints, and other features. We will
 discuss its other applications later. Regarding aliases,
 the following command creates aliases for all objects starting with
@@ -70,7 +70,7 @@ the following command creates aliases for all objects starting with
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
   check ge -- display the type of nat.ge
 #+END_SRC
 
@@ -79,11 +79,11 @@ that =n=, =m= and =o= have type =nat=.
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
   variable n : nat
   variable m : nat
   variable o : nat
-  -- The command 'using nat' also imported the notation defined at the namespace 'nat'
+  -- The command 'open nat' also imported the notation defined at the namespace 'nat'
   check n + m
   check n ≤ m
 #+END_SRC
@@ -96,7 +96,7 @@ for =n = n=. In Lean, =refl= is the reflexivity theorem.
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
   variable n : nat
   check refl n
 #+END_SRC
@@ -108,7 +108,7 @@ The following commands postulate two axioms =Ax1= and =Ax2= that state that =n =
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
   variables m n o : nat
   axiom Ax1 : n = m
   axiom Ax2 : m = o
@@ -146,7 +146,7 @@ example, =symm= is the symmetry theorem.
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
 
   theorem nat_trans3 (a b c d : nat) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
   trans (trans H1 (symm H2)) H3
@@ -175,7 +175,7 @@ implicit arguments.
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
 
   theorem nat_trans3i {a b c d : nat} (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
   trans (trans H1 (symm H2)) H3
@@ -210,7 +210,7 @@ This is useful when debugging non-trivial problems.
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
 
   variables a b c : nat
   axiom H1 : a = b
@@ -361,7 +361,7 @@ examples.
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
 
   check fun x : nat, x + 1
   check fun x y : nat, x + 2 * y
@@ -375,7 +375,7 @@ In all examples above, the type can be inferred automatically.
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
 
   check fun x, x + 1
   check fun x y, x + 2 * y
@@ -392,7 +392,7 @@ function applications
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
   check (fun x y, x + 2 * y) 1
   check (fun x y, x + 2 * y) 1 2
   check (fun x y, not (x ∧ y)) true false
@@ -420,7 +420,7 @@ are equal using just =refl=. Here is a simple example.
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
 
   theorem def_eq_th (a : nat) : ((λ x : nat, x + 1) a) = a + 1 := refl (a+1)
 #+END_SRC
@@ -652,7 +652,7 @@ Then we instantiate the axiom using function application.
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
 
   variable f : nat → nat
   axiom fzero : ∀ x, f x = 0
@@ -668,7 +668,7 @@ abstraction. In the following example, we create a proof term showing that for a
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
 
   variable f : nat → nat
   axiom fzero : ∀ x, f x = 0
@@ -693,7 +693,7 @@ for =∃ a : nat, a = w= using
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
 
   theorem nat_trans3i {a b c d : nat} (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
   trans (trans H1 (symm H2)) H3
@@ -720,7 +720,7 @@ has different values for the implicit argument =P=.
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
 
   check @exists_intro
   variable g : nat → nat → nat
@@ -751,7 +751,7 @@ of two even numbers is an even number.
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
 
   definition even (a : nat) := ∃ b, a = 2*b
   theorem EvenPlusEven {a b : nat} (H1 : even a) (H2 : even b) : even (a + b) :=
@@ -772,7 +772,7 @@ With this macro we can write the example above in a more natural way
 
 #+BEGIN_SRC lean
   import data.nat
-  using nat
+  open nat
   definition even (a : nat) := ∃ b, a = 2*b
   theorem EvenPlusEven {a b : nat} (H1 : even a) (H2 : even b) : even (a + b) :=
   obtain (w1 : nat) (Hw1 : a = 2*w1), from H1,
diff --git a/library/data/bool.lean b/library/data/bool.lean
index d6aca2af4..40f07b5f8 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -4,7 +4,7 @@
 
 import logic.core.connectives logic.classes.decidable logic.classes.inhabited
 
-using eq_ops decidable
+open eq_ops decidable
 
 inductive bool : Type :=
 ff : bool,
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index ee6666e98..37cb7af22 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -11,20 +11,13 @@ import ..nat.basic ..nat.order ..nat.sub ..prod ..quotient ..quotient tools.tact
 import struc.binary
 import tools.fake_simplifier
 
-using nat (hiding case)
-using quotient
-using subtype
-using prod
-using relation
-using decidable
-using binary
-using fake_simplifier
-using eq_ops
+open nat (hiding case)
+open quotient subtype prod relation
+open decidable binary fake_simplifier
+open eq_ops
+
 namespace int
-
-
 -- ## The defining equivalence relation on ℕ × ℕ
-
 abbreviation rel (a b : ℕ × ℕ) : Prop :=  pr1 a + pr2 b = pr2 a + pr1 b
 
 theorem rel_comp (n m k l : ℕ) : (rel (pair n m) (pair k l)) ↔ (n + l = m + k) :=
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 33bc9999c..b5d6098d6 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -9,10 +9,10 @@
 
 import .basic
 
-using nat (hiding case)
-using decidable
-using fake_simplifier
-using int eq_ops
+open nat (hiding case)
+open decidable
+open fake_simplifier
+open int eq_ops
 
 namespace int
 
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 41c7ea713..8b0006399 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -14,9 +14,9 @@ import data.nat
 import logic tools.helper_tactics
 -- import if -- for find
 
-using nat
-using eq_ops
-using helper_tactics
+open nat
+open eq_ops
+open helper_tactics
 
 namespace list
 
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index b9bffcecc..e5c2f0e0e 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -9,10 +9,10 @@
 
 import logic data.num tools.tactic struc.binary tools.helper_tactics
 
-using num tactic binary eq_ops
-using decidable (hiding induction_on rec_on)
-using relation -- for subst_iff
-using helper_tactics
+open num tactic binary eq_ops
+open decidable (hiding induction_on rec_on)
+open relation -- for subst_iff
+open helper_tactics
 
 -- Definition of the type
 -- ----------------------
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 99678953f..9714d0e70 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -11,9 +11,9 @@
 import logic .sub struc.relation data.prod
 import tools.fake_simplifier
 
-using nat relation relation.iff_ops prod
-using fake_simplifier decidable
-using eq_ops
+open nat relation relation.iff_ops prod
+open fake_simplifier decidable
+open eq_ops
 
 namespace nat
 
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 98a27b52f..7b586ccc4 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -10,9 +10,9 @@
 import .basic logic.classes.decidable
 import tools.fake_simplifier
 
-using nat eq_ops tactic
-using fake_simplifier
-using decidable (decidable inl inr)
+open nat eq_ops tactic
+open fake_simplifier
+open decidable (decidable inl inr)
 
 namespace nat
 
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index 02d0a065e..1764eb156 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -10,9 +10,9 @@
 import data.nat.order
 import tools.fake_simplifier
 
-using nat eq_ops tactic
-using helper_tactics
-using fake_simplifier
+open nat eq_ops tactic
+open helper_tactics
+open fake_simplifier
 
 namespace nat
 
diff --git a/library/data/option.lean b/library/data/option.lean
index 5417aae8e..7286ace55 100644
--- a/library/data/option.lean
+++ b/library/data/option.lean
@@ -3,7 +3,7 @@
 -- Author: Leonardo de Moura
 
 import logic.core.eq logic.classes.inhabited logic.classes.decidable
-using eq_ops decidable
+open eq_ops decidable
 
 namespace option
 
diff --git a/library/data/prod.lean b/library/data/prod.lean
index 3821e7cc7..02b350586 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -9,7 +9,7 @@
 
 import logic.classes.inhabited logic.core.eq logic.classes.decidable
 
-using inhabited decidable
+open inhabited decidable
 
 inductive prod (A B : Type) : Type :=
 pair : A → B → prod A B
diff --git a/library/data/quotient/aux.lean b/library/data/quotient/aux.lean
index 07dcc3055..896ad88ee 100644
--- a/library/data/quotient/aux.lean
+++ b/library/data/quotient/aux.lean
@@ -5,8 +5,8 @@
 import logic ..prod struc.relation
 import tools.fake_simplifier
 
-using prod eq_ops
-using fake_simplifier
+open prod eq_ops
+open fake_simplifier
 
 namespace quotient
 
diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean
index 4606c0bcd..f61a4d5f8 100644
--- a/library/data/quotient/basic.lean
+++ b/library/data/quotient/basic.lean
@@ -9,8 +9,8 @@ import logic tools.tactic ..subtype logic.core.cast struc.relation data.prod
 import logic.core.instances
 import .aux
 
-using relation prod inhabited nonempty tactic eq_ops
-using subtype relation.iff_ops
+open relation prod inhabited nonempty tactic eq_ops
+open subtype relation.iff_ops
 
 namespace quotient
 
diff --git a/library/data/quotient/classical.lean b/library/data/quotient/classical.lean
index ba234cb7a..b53903c1d 100644
--- a/library/data/quotient/classical.lean
+++ b/library/data/quotient/classical.lean
@@ -8,7 +8,7 @@ import logic.axioms.classical logic.axioms.hilbert logic.axioms.funext
 
 namespace quotient
 
-using relation nonempty subtype
+open relation nonempty subtype
 
 -- abstract quotient
 -- -----------------
diff --git a/library/data/set.lean b/library/data/set.lean
index 3adae8531..9b3c060bc 100644
--- a/library/data/set.lean
+++ b/library/data/set.lean
@@ -4,7 +4,7 @@
 --- Author: Jeremy Avigad, Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
 import data.bool
-using eq_ops bool
+open eq_ops bool
 
 namespace set
 definition set (T : Type) :=
diff --git a/library/data/sigma.lean b/library/data/sigma.lean
index d18cc966b..8c15151ac 100644
--- a/library/data/sigma.lean
+++ b/library/data/sigma.lean
@@ -4,7 +4,7 @@
 
 import logic.classes.inhabited logic.core.eq
 
-using inhabited
+open inhabited
 
 inductive sigma {A : Type} (B : A → Type) : Type :=
 dpair : Πx : A, B x → sigma B
diff --git a/library/data/string.lean b/library/data/string.lean
index 464c8521e..9c73b2412 100644
--- a/library/data/string.lean
+++ b/library/data/string.lean
@@ -4,7 +4,7 @@
 
 import data.bool
 
-using bool inhabited
+open bool inhabited
 
 namespace string
 
diff --git a/library/data/subtype.lean b/library/data/subtype.lean
index 2a204b878..cd8af4407 100644
--- a/library/data/subtype.lean
+++ b/library/data/subtype.lean
@@ -4,7 +4,7 @@
 
 import logic.classes.inhabited logic.core.eq logic.classes.decidable
 
-using decidable
+open decidable
 
 inductive subtype {A : Type} (P : A → Prop) : Type :=
 tag : Πx : A, P x → subtype P
diff --git a/library/data/sum.lean b/library/data/sum.lean
index 2abba99a4..931c6e2d0 100644
--- a/library/data/sum.lean
+++ b/library/data/sum.lean
@@ -9,7 +9,7 @@
 
 import logic.core.prop logic.classes.inhabited logic.classes.decidable
 
-using inhabited decidable
+open inhabited decidable
 
 namespace sum
 
diff --git a/library/data/unit.lean b/library/data/unit.lean
index 286cc23c2..19dfca8d8 100644
--- a/library/data/unit.lean
+++ b/library/data/unit.lean
@@ -4,7 +4,7 @@
 
 import logic.classes.decidable logic.classes.inhabited
 
-using decidable
+open decidable
 
 namespace unit
 
diff --git a/library/hott/fibrant.lean b/library/hott/fibrant.lean
index 16a357af7..3f5606bf9 100644
--- a/library/hott/fibrant.lean
+++ b/library/hott/fibrant.lean
@@ -5,7 +5,7 @@
 import data.unit data.bool data.nat
 import data.prod data.sum data.sigma
 
-using unit bool nat prod sum sigma
+open unit bool nat prod sum sigma
 
 inductive fibrant (T : Type) : Type :=
 fibrant_mk : fibrant T
@@ -32,4 +32,4 @@ instance pi_fibrant
 
 theorem test_fibrant : fibrant (nat × (nat ⊎ nat)) := _
 
-end fibrant
\ No newline at end of file
+end fibrant
diff --git a/library/hott/path.lean b/library/hott/path.lean
index b47568dce..ab7d2fa78 100644
--- a/library/hott/path.lean
+++ b/library/hott/path.lean
@@ -10,7 +10,7 @@
 
 import general_notation struc.function
 
-using function
+open function
 
 -- Path
 -- ----
@@ -30,7 +30,7 @@ end path
 
 
 -- TODO: should all this be in namespace path?
-using path (induction_on)
+open path (induction_on)
 
 -- Concatenation and inverse
 -- -------------------------
diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean
index 805cc8043..da1fa57bf 100644
--- a/library/logic/axioms/classical.lean
+++ b/library/logic/axioms/classical.lean
@@ -7,7 +7,7 @@
 
 import logic.core.quantifiers logic.core.cast struc.relation
 
-using eq_ops
+open eq_ops
 
 axiom prop_complete (a : Prop) : a = true ∨ a = false
 
@@ -48,7 +48,7 @@ propext
   (assume H, iff_to_eq H)
   (assume H, eq_to_iff H)
 
-using relation
+open relation
 theorem iff_congruence [instance] (P : Prop → Prop) : congruence iff iff P :=
 congruence_mk
   (take (a b : Prop),
diff --git a/library/logic/axioms/examples/diaconescu.lean b/library/logic/axioms/examples/diaconescu.lean
index cbfae2fb0..3b28bfcb1 100644
--- a/library/logic/axioms/examples/diaconescu.lean
+++ b/library/logic/axioms/examples/diaconescu.lean
@@ -3,7 +3,7 @@
 -- Author: Leonardo de Moura
 
 import logic.axioms.hilbert logic.axioms.funext
-using eq_ops nonempty inhabited
+open eq_ops nonempty inhabited
 
 -- Diaconescu’s theorem
 -- Show that Excluded middle follows from
diff --git a/library/logic/axioms/funext.lean b/library/logic/axioms/funext.lean
index 86dfcef8a..4cf47ae41 100644
--- a/library/logic/axioms/funext.lean
+++ b/library/logic/axioms/funext.lean
@@ -5,7 +5,7 @@
 ----------------------------------------------------------------------------------------------------
 
 import logic.core.eq struc.function
-using function
+open function
 
 -- Function extensionality
 axiom funext : ∀ {A : Type} {B : A → Type} {f g : Π x, B x} (H : ∀ x, f x = g x), f = g
diff --git a/library/logic/axioms/hilbert.lean b/library/logic/axioms/hilbert.lean
index e62bb72d1..db62aa086 100644
--- a/library/logic/axioms/hilbert.lean
+++ b/library/logic/axioms/hilbert.lean
@@ -12,7 +12,7 @@ import logic.core.quantifiers
 import logic.classes.inhabited logic.classes.nonempty
 import data.subtype data.sum
 
-using subtype inhabited nonempty
+open subtype inhabited nonempty
 
 
 -- the axiom
diff --git a/library/logic/axioms/piext.lean b/library/logic/axioms/piext.lean
index de74d159c..db6e21128 100644
--- a/library/logic/axioms/piext.lean
+++ b/library/logic/axioms/piext.lean
@@ -6,7 +6,7 @@
 
 import logic.classes.inhabited logic.core.cast
 
-using inhabited
+open inhabited
 
 -- Pi extensionality
 axiom piext {A : Type} {B B' : A → Type} {H : inhabited (Π x, B x)} :
diff --git a/library/logic/axioms/prop_decidable.lean b/library/logic/axioms/prop_decidable.lean
index d575875bc..43ff8f809 100644
--- a/library/logic/axioms/prop_decidable.lean
+++ b/library/logic/axioms/prop_decidable.lean
@@ -6,7 +6,7 @@
 -- ===========================
 
 import logic.axioms.classical logic.axioms.hilbert logic.classes.decidable
-using decidable inhabited nonempty
+open decidable inhabited nonempty
 
 -- Excluded middle + Hilbert implies every proposition is decidable
 
diff --git a/library/logic/classes/nonempty.lean b/library/logic/classes/nonempty.lean
index 3a446b825..5ed93edca 100644
--- a/library/logic/classes/nonempty.lean
+++ b/library/logic/classes/nonempty.lean
@@ -4,7 +4,7 @@
 
 import .inhabited
 
-using inhabited
+open inhabited
 
 namespace nonempty
 
diff --git a/library/logic/core/cast.lean b/library/logic/core/cast.lean
index 748e05b10..afe8d8ad0 100644
--- a/library/logic/core/cast.lean
+++ b/library/logic/core/cast.lean
@@ -6,7 +6,7 @@
 
 import .eq .quantifiers
 
-using eq_ops
+open eq_ops
 
 definition cast {A B : Type} (H : A = B) (a : A) : B :=
 eq_rec a H
diff --git a/library/logic/core/eq.lean b/library/logic/core/eq.lean
index 235e86746..d4c32dfea 100644
--- a/library/logic/core/eq.lean
+++ b/library/logic/core/eq.lean
@@ -40,7 +40,7 @@ namespace eq_ops
   infixr `⬝`   := trans
   infixr `▸`   := subst
 end eq_ops
-using eq_ops
+open eq_ops
 
 theorem true_ne_false : ¬true = false :=
 assume H : true = false,
diff --git a/library/logic/core/examples/instances_test.lean b/library/logic/core/examples/instances_test.lean
index 6ff3006e7..a41e99b30 100644
--- a/library/logic/core/examples/instances_test.lean
+++ b/library/logic/core/examples/instances_test.lean
@@ -4,11 +4,10 @@
 
 import ..instances
 
-using relation
-
-using relation.general_operations
-using relation.iff_ops
-using eq_ops
+open relation
+open relation.general_operations
+open relation.iff_ops
+open eq_ops
 
 section
 
diff --git a/library/logic/core/identities.lean b/library/logic/core/identities.lean
index df0d970ba..79050a4a6 100644
--- a/library/logic/core/identities.lean
+++ b/library/logic/core/identities.lean
@@ -10,7 +10,7 @@
 
 import logic.core.instances logic.classes.decidable logic.core.quantifiers logic.core.cast
 
-using relation decidable relation.iff_ops
+open relation decidable relation.iff_ops
 
 theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
 calc
diff --git a/library/logic/core/if.lean b/library/logic/core/if.lean
index 8b24df6df..75aa8390c 100644
--- a/library/logic/core/if.lean
+++ b/library/logic/core/if.lean
@@ -5,7 +5,7 @@
 ----------------------------------------------------------------------------------------------------
 
 import logic.classes.decidable tools.tactic
-using decidable tactic eq_ops
+open decidable tactic eq_ops
 
 definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A :=
 decidable.rec_on H (assume Hc,  t) (assume Hnc, e)
diff --git a/library/logic/core/instances.lean b/library/logic/core/instances.lean
index 3aceca80b..5ad8671ff 100644
--- a/library/logic/core/instances.lean
+++ b/library/logic/core/instances.lean
@@ -9,7 +9,7 @@ import logic.core.connectives struc.relation
 
 namespace relation
 
-using relation
+open relation
 
 -- Congruences for logic
 -- ---------------------
diff --git a/library/logic/core/quantifiers.lean b/library/logic/core/quantifiers.lean
index 6f7239eee..8cce88069 100644
--- a/library/logic/core/quantifiers.lean
+++ b/library/logic/core/quantifiers.lean
@@ -4,7 +4,7 @@
 
 import .connectives ..classes.nonempty
 
-using inhabited nonempty
+open inhabited nonempty
 
 inductive Exists {A : Type} (P : A → Prop) : Prop :=
 exists_intro : ∀ (a : A), P a → Exists P
diff --git a/library/struc/binary.lean b/library/struc/binary.lean
index f6755aa0a..cb60d8d12 100644
--- a/library/struc/binary.lean
+++ b/library/struc/binary.lean
@@ -1,9 +1,8 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-
 import logic.core.eq
-using eq_ops
+open eq_ops
 
 namespace binary
 section
diff --git a/library/struc/wf.lean b/library/struc/wf.lean
index 17e2254e8..bd1b7484b 100644
--- a/library/struc/wf.lean
+++ b/library/struc/wf.lean
@@ -5,7 +5,7 @@
 import logic.axioms.classical logic.axioms.prop_decidable logic.classes.decidable
 import logic.core.identities
 
-using decidable
+open decidable
 
 -- Well-founded relation definition
 -- We are essentially saying that a relation R is well-founded
diff --git a/library/tools/fake_simplifier.lean b/library/tools/fake_simplifier.lean
index 28140299d..ca4b09c77 100644
--- a/library/tools/fake_simplifier.lean
+++ b/library/tools/fake_simplifier.lean
@@ -1,5 +1,5 @@
 import .tactic
-using tactic
+open tactic
 
 namespace fake_simplifier
 
diff --git a/library/tools/helper_tactics.lean b/library/tools/helper_tactics.lean
index 83178f734..5bad61330 100644
--- a/library/tools/helper_tactics.lean
+++ b/library/tools/helper_tactics.lean
@@ -9,7 +9,7 @@
 
 import .tactic
 
-using tactic
+open tactic
 
 namespace helper_tactics
   definition apply_refl := apply @refl
diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean
index 1e3b79e39..08513d43f 100644
--- a/library/tools/tactic.lean
+++ b/library/tools/tactic.lean
@@ -5,8 +5,8 @@
 ----------------------------------------------------------------------------------------------------
 
 import data.string data.num
-using string
-using num
+open string
+open num
 
 namespace tactic
 -- This is just a trick to embed the 'tactic language' as a
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 09cea3682..9930a1973 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -11,7 +11,7 @@
   '("import" "abbreviation" "opaque_hint" "tactic_hint" "definition" "renaming"
     "inline" "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture"
     "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem"
-    "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment"
+    "context" "open" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment"
     "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl"
     "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
     "private" "using" "namespace" "builtin" "including" "instance" "class" "section"
@@ -60,10 +60,6 @@
      ;; Constants
      (,(rx (or "#" "@" "->" "∼" "↔" "/" "==" "=" ":=" "<->" "/\\" "\\/" "∧" "∨" "≠" "<" ">" "≤" "≥" "¬" "<=" ">=" "⁻¹" "⬝" "▸" "+" "*" "-" "/")) . 'font-lock-constant-face)
      (,(rx (or "λ" "→" "∃" "∀" ":=")) . 'font-lock-constant-face )
-     (,(rx symbol-start
-           (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "back" "beta" "done" "exact")
-           symbol-end)
-      . 'font-lock-constant-face)
      ;; universe/inductive/theorem... "names"
      (,(rx symbol-start
            (group (or "universe" "inductive" "theorem" "axiom" "lemma" "hypothesis"
@@ -76,7 +72,12 @@
      ;; place holder
      (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
      ;; modifiers
-     (,(rx (or "\[protected\]" "\[private\]" "\[instance\]" "\[coercion\]" "\[inline\]")) . 'font-lock-doc-face)
+     (,(rx (or "\[notation\]" "\[protected\]" "\[private\]" "\[instance\]" "\[coercion\]" "\[inline\]")) . 'font-lock-doc-face)
+     ;; tactics
+     (,(rx symbol-start
+           (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "back" "beta" "done" "exact" "repeat")
+           symbol-end)
+      . 'font-lock-constant-face)
      ;; sorry
      (,(rx symbol-start "sorry" symbol-end) . 'font-lock-warning-face)
      ;; ? query
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index d44b601a9..c4e96a7d6 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -166,9 +166,9 @@ static name parse_class(parser & p) {
         else if (p.curr_is_keyword() || p.curr_is_command())
             n = p.get_token_info().value();
         else
-            throw parser_error("invalid 'using' command, identifier or symbol expected", p.pos());
+            throw parser_error("invalid 'open' command, identifier or symbol expected", p.pos());
         p.next();
-        p.check_token_next(g_rbracket, "invalid 'using' command, ']' expected");
+        p.check_token_next(g_rbracket, "invalid 'open' command, ']' expected");
         return n;
     } else {
         return name();
@@ -178,17 +178,17 @@ static name parse_class(parser & p) {
 static void check_identifier(parser & p, environment const & env, name const & ns, name const & id) {
     name full_id = ns + id;
     if (!env.find(full_id))
-        throw parser_error(sstream() << "invalid 'using' command, unknown declaration '" << full_id << "'", p.pos());
+        throw parser_error(sstream() << "invalid 'open' command, unknown declaration '" << full_id << "'", p.pos());
 }
 
-// using [class] id (id ...) (renaming id->id id->id) (hiding id ... id)
-environment using_cmd(parser & p) {
+// open [class] id (id ...) (renaming id->id id->id) (hiding id ... id)
+environment open_cmd(parser & p) {
     environment env = p.env();
     while (true) {
         name cls = parse_class(p);
         bool decls = cls.is_anonymous() || cls == g_decls || cls == g_declarations;
         auto pos   = p.pos();
-        name ns    = p.check_id_next("invalid 'using' command, identifier expected");
+        name ns    = p.check_id_next("invalid 'open' command, identifier expected");
         optional<name> real_ns = to_valid_namespace_name(env, ns);
         if (!real_ns)
             throw parser_error(sstream() << "invalid namespace name '" << ns << "'", pos);
@@ -205,8 +205,8 @@ environment using_cmd(parser & p) {
                     while (p.curr_is_identifier()) {
                         name from_id = p.get_name_val();
                         p.next();
-                        p.check_token_next(g_arrow, "invalid 'using' command renaming, '->' expected");
-                        name to_id = p.check_id_next("invalid 'using' command renaming, identifier expected");
+                        p.check_token_next(g_arrow, "invalid 'open' command renaming, '->' expected");
+                        name to_id = p.check_id_next("invalid 'open' command renaming, identifier expected");
                         check_identifier(p, env, ns, from_id);
                         exceptions.push_back(from_id);
                         env = add_expr_alias(env, to_id, ns+from_id);
@@ -228,11 +228,11 @@ environment using_cmd(parser & p) {
                         env = add_expr_alias(env, id, ns+id);
                     }
                 } else {
-                    throw parser_error("invalid 'using' command option, identifier, 'hiding' or 'renaming' expected", p.pos());
+                    throw parser_error("invalid 'open' command option, identifier, 'hiding' or 'renaming' expected", p.pos());
                 }
                 if (found_explicit && !exceptions.empty())
-                    throw parser_error("invalid 'using' command option, mixing explicit and implicit 'using' options", p.pos());
-                p.check_token_next(g_rparen, "invalid 'using' command option, ')' expected");
+                    throw parser_error("invalid 'open' command option, mixing explicit and implicit 'open' options", p.pos());
+                p.check_token_next(g_rparen, "invalid 'open' command option, ')' expected");
             }
             if (!found_explicit)
                 env = add_aliases(env, ns, name(), exceptions.size(), exceptions.data());
@@ -303,7 +303,7 @@ environment erase_cache_cmd(parser & p) {
 
 cmd_table init_cmd_table() {
     cmd_table r;
-    add_cmd(r, cmd_info("using",        "create aliases for declarations, and use objects defined in other namespaces", using_cmd));
+    add_cmd(r, cmd_info("open",         "create aliases for declarations, and use objects defined in other namespaces", open_cmd));
     add_cmd(r, cmd_info("set_option",   "set configuration option", set_option_cmd));
     add_cmd(r, cmd_info("exit",         "exit", exit_cmd));
     add_cmd(r, cmd_info("print",        "print a string", print_cmd));
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 7cab355ea..858a53555 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -68,7 +68,7 @@ token_table init_token_table() {
     pair<char const *, unsigned> builtin[] =
         {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"obtain", 0}, {"by", 0}, {"then", 0},
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
-         {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type'", g_max_prec},
+         {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type'", g_max_prec}, {"using", 0},
          {"|", 0}, {"!", 0}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec},
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
@@ -78,7 +78,7 @@ token_table init_token_table() {
                                "abbreviation", "opaque_hint", "evaluate", "check", "print", "end", "namespace", "section", "import",
                                "abbreviation", "inductive", "record", "renaming", "extends", "structure", "module", "universe",
                                "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
-                               "exit", "set_option", "using", "calc_subst", "calc_refl", "calc_trans", "tactic_hint",
+                               "exit", "set_option", "open", "calc_subst", "calc_refl", "calc_trans", "tactic_hint",
                                "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "#erase_cache", nullptr};
 
     pair<char const *, char const *> aliases[] =
diff --git a/tests/lean/alias.lean b/tests/lean/alias.lean
index dbcaee8a3..93c9db7dd 100644
--- a/tests/lean/alias.lean
+++ b/tests/lean/alias.lean
@@ -10,16 +10,15 @@ namespace N2
   variable foo : val → val → val
 end N2
 
-using N2
-using N1
+open N2
+open N1
 variables a b : num
 print raw foo a b
-using N2
+open N2
 print raw foo a b
-using N1
+open N1
 print raw foo a b
-using N1
+open N1
 print raw foo a b
-using N2
+open N2
 print raw foo a b
-
diff --git a/tests/lean/choice_expl.lean b/tests/lean/choice_expl.lean
index c013f5df3..e06623b5c 100644
--- a/tests/lean/choice_expl.lean
+++ b/tests/lean/choice_expl.lean
@@ -6,7 +6,7 @@ namespace N2
   definition pr {A : Type} (a b : A) := b
 end N2
 
-using N1 N2
+open N1 N2
 variable N : Type.{1}
 variables a b : N
 check @pr
diff --git a/tests/lean/empty.lean b/tests/lean/empty.lean
index afe98af98..d0e7e2f80 100644
--- a/tests/lean/empty.lean
+++ b/tests/lean/empty.lean
@@ -1,5 +1,5 @@
 import logic logic.axioms.hilbert
-using inhabited nonempty
+open inhabited nonempty
 
 definition v1 : Prop := epsilon (λ x, true)
 inductive Empty : Type
diff --git a/tests/lean/empty_thm.lean b/tests/lean/empty_thm.lean
index 11af2d267..07e0611a1 100644
--- a/tests/lean/empty_thm.lean
+++ b/tests/lean/empty_thm.lean
@@ -1,5 +1,5 @@
 import logic tools.tactic
-using tactic
+open tactic
 
 definition simple := apply trivial
 
diff --git a/tests/lean/have1.lean b/tests/lean/have1.lean
index e4be7dc7c..bcaec8ce6 100644
--- a/tests/lean/have1.lean
+++ b/tests/lean/have1.lean
@@ -1,5 +1,5 @@
 import logic
-using bool eq_ops tactic
+open bool eq_ops tactic
 
 variables a b c : bool
 axiom H1 : a = b
diff --git a/tests/lean/interactive/class_bug.lean b/tests/lean/interactive/class_bug.lean
index 9e08974e7..414181cae 100644
--- a/tests/lean/interactive/class_bug.lean
+++ b/tests/lean/interactive/class_bug.lean
@@ -1,5 +1,5 @@
 import logic.axioms.hilbert data.nat.basic
-using nonempty inhabited nat
+open nonempty inhabited nat
 
 theorem int_inhabited [instance] : inhabited nat := inhabited_mk zero
 
diff --git a/tests/lean/let3.lean b/tests/lean/let3.lean
index 83dd47078..b4e9babd8 100644
--- a/tests/lean/let3.lean
+++ b/tests/lean/let3.lean
@@ -1,5 +1,5 @@
 import data.num
-using num
+open num
 
 variable f : num → num → num → num
 
diff --git a/tests/lean/let4.lean b/tests/lean/let4.lean
index 9b765e4e0..1c1817cca 100644
--- a/tests/lean/let4.lean
+++ b/tests/lean/let4.lean
@@ -1,5 +1,5 @@
 import data.num
-using num
+open num
 
 variable f : num → num → num → num
 
@@ -15,5 +15,3 @@ check
       d := 10,
       e := f (f 10 10 d) (f d 10 10) a
   in f a b (f e d 10)
-
-
diff --git a/tests/lean/num.lean b/tests/lean/num.lean
index bcde80f7b..d431a69db 100644
--- a/tests/lean/num.lean
+++ b/tests/lean/num.lean
@@ -1,5 +1,5 @@
 import data.num
-using num
+open num
 
 check 10
 check 20
diff --git a/tests/lean/protected.lean b/tests/lean/protected.lean
index e0ab83a02..edc1d14d6 100644
--- a/tests/lean/protected.lean
+++ b/tests/lean/protected.lean
@@ -5,6 +5,6 @@ namespace foo
   definition D := true
 end foo
 
-using foo
+open foo
 check C
 check D
diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean
index 8f19a3dbc..40a8d2779 100644
--- a/tests/lean/run/algebra1.lean
+++ b/tests/lean/run/algebra1.lean
@@ -1,5 +1,5 @@
 import logic
-using num
+open num
 
 abbreviation Type1 := Type.{1}
 
@@ -88,7 +88,7 @@ namespace monoid
   definition assoc [inline] {A : Type} (s : monoid_struct A) : is_assoc (mul s)
   := monoid_struct_rec (fun mul id a i, a) s
 
-  using semigroup
+  open semigroup
   definition is_semigroup_struct [inline] [instance] (A : Type) (s : monoid_struct A) : semigroup_struct A
   := mk_semigroup_struct (mul s) (assoc s)
 
@@ -104,7 +104,7 @@ end monoid
 end algebra
 
 section
-  using algebra algebra.semigroup algebra.monoid
+  open algebra algebra.semigroup algebra.monoid
   variable M : monoid
   variables a b c : M
   check a*b*c*a*b*c*a*b*a*b*c*a
diff --git a/tests/lean/run/alias1.lean b/tests/lean/run/alias1.lean
index b2163ab49..b3b1a4eeb 100644
--- a/tests/lean/run/alias1.lean
+++ b/tests/lean/run/alias1.lean
@@ -10,8 +10,8 @@ namespace N2
   variable foo : val → val → val
 end N2
 
-using N1
-using N2
+open N1
+open N2
 variables a b : num
 variables x y : val
 
@@ -35,7 +35,7 @@ definition aux1 := foo a b  -- System elaborated it to N1.foo a b
 theorem T2 : aux1 = N1.foo a b
 := refl _
 
-using N1
+open N1
 definition aux2 := foo a b  -- Now N1 is in the end of the queue, this is elaborated to N2.foo (f a) (f b)
 check aux2
 
diff --git a/tests/lean/run/alias2.lean b/tests/lean/run/alias2.lean
index 7ebca4252..ad27b49a5 100644
--- a/tests/lean/run/alias2.lean
+++ b/tests/lean/run/alias2.lean
@@ -10,8 +10,8 @@ namespace N2
   variable foo : val → val → val
 end N2
 
-using N1
-using N2
+open N1
+open N2
 variables a b : num
 variable f : num → val
 coercion f
@@ -20,4 +20,3 @@ definition aux2 := foo a b
 check aux2
 theorem T3 : aux2 = N1.foo a b
 := refl _
-
diff --git a/tests/lean/run/booltst.lean b/tests/lean/run/booltst.lean
index cd6c1d2f5..b0359ead0 100644
--- a/tests/lean/run/booltst.lean
+++ b/tests/lean/run/booltst.lean
@@ -1,4 +1,4 @@
 import data.bool
-using bool
+open bool
 
-check ff
\ No newline at end of file
+check ff
diff --git a/tests/lean/run/calc.lean b/tests/lean/run/calc.lean
index 43c2848cf..513fa3f57 100644
--- a/tests/lean/run/calc.lean
+++ b/tests/lean/run/calc.lean
@@ -1,5 +1,5 @@
 import data.num
-using num
+open num
 
 namespace foo
   variable le : num → num → Prop
diff --git a/tests/lean/run/choice_ctx.lean b/tests/lean/run/choice_ctx.lean
index 8c4d82299..479d9110d 100644
--- a/tests/lean/run/choice_ctx.lean
+++ b/tests/lean/run/choice_ctx.lean
@@ -1,5 +1,5 @@
 import data.nat.basic
-using nat
+open nat
 
 set_option pp.coercion true
 
@@ -8,7 +8,7 @@ theorem trans {a b c : nat} (H1 : a = b) (H2 : b = c) : a = c :=
 trans H1 H2
 end foo
 
-using foo
+open foo
 
 theorem tst (a b : nat) (H0 : b = a) (H : b = 0) : a = 0
 := have H1 : a = b, from symm H0,
@@ -17,4 +17,3 @@ theorem tst (a b : nat) (H0 : b = a) (H : b = 0) : a = 0
 definition f (a b : nat) :=
 let x := 3 in
 a + x
-
diff --git a/tests/lean/run/class1.lean b/tests/lean/run/class1.lean
index 8c01c706f..c7b2dc17b 100644
--- a/tests/lean/run/class1.lean
+++ b/tests/lean/run/class1.lean
@@ -1,5 +1,5 @@
 import logic data.prod
-using num prod inhabited
+open num prod inhabited
 
 definition H : inhabited (Prop × num × (num → num)) := _
 
diff --git a/tests/lean/run/class2.lean b/tests/lean/run/class2.lean
index 5d4ae9feb..95554944a 100644
--- a/tests/lean/run/class2.lean
+++ b/tests/lean/run/class2.lean
@@ -1,5 +1,5 @@
 import logic data.prod
-using num prod nonempty inhabited
+open num prod nonempty inhabited
 
 theorem H {A B : Type} (H1 : inhabited A) : inhabited (Prop × A × (B → num))
 := _
diff --git a/tests/lean/run/class3.lean b/tests/lean/run/class3.lean
index 6a1af65c7..b4c655a0e 100644
--- a/tests/lean/run/class3.lean
+++ b/tests/lean/run/class3.lean
@@ -1,5 +1,5 @@
 import logic data.prod
-using num prod inhabited
+open num prod inhabited
 
 section
   parameter {A : Type}
diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean
index 8dc09c2a0..bd16d2d11 100644
--- a/tests/lean/run/class5.lean
+++ b/tests/lean/run/class5.lean
@@ -23,36 +23,36 @@ namespace nat
 end nat
 
 section
-  using algebra nat
+  open algebra nat
   variables a b c : nat
   check a * b * c
   definition tst1 : nat := a * b * c
 end
 
 section
-  using [notation] algebra
-  using nat
-  -- check mul_struct nat  << This is an error, we are using only the notation from algebra
+  open [notation] algebra
+  open nat
+  -- check mul_struct nat  << This is an error, we are open only the notation from algebra
   variables a b c : nat
   check a * b * c
   definition tst2 : nat := a * b * c
 end
 
 section
-  using nat
-  -- check mul_struct nat  << This is an error, we are using only the notation from algebra
+  open nat
+  -- check mul_struct nat  << This is an error, we are open only the notation from algebra
   variables a b c : nat
   check #algebra a*b*c
   definition tst3 : nat := #algebra a*b*c
 end
 
 section
-  using nat
+  open nat
   set_option pp.implicit true
   definition add_struct [instance] : algebra.mul_struct nat
   := algebra.mk_mul_struct add
 
   variables a b c : nat
-  check #algebra a*b*c  -- << is using add instead of mul
+  check #algebra a*b*c  -- << is open add instead of mul
   definition tst4 : nat := #algebra a*b*c
 end
diff --git a/tests/lean/run/class6.lean b/tests/lean/run/class6.lean
index 9485c6e37..5e31b412e 100644
--- a/tests/lean/run/class6.lean
+++ b/tests/lean/run/class6.lean
@@ -1,5 +1,5 @@
 import logic data.prod
-using prod
+open prod
 
 inductive t1 : Type :=
 mk1 : t1
diff --git a/tests/lean/run/class7.lean b/tests/lean/run/class7.lean
index cba9a37cf..a77db343b 100644
--- a/tests/lean/run/class7.lean
+++ b/tests/lean/run/class7.lean
@@ -1,5 +1,5 @@
 import logic
-using num tactic
+open num tactic
 
 inductive inh (A : Type) : Type :=
 inh_intro : A -> inh A
diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean
index d1b2809a8..2716a54ef 100644
--- a/tests/lean/run/class8.lean
+++ b/tests/lean/run/class8.lean
@@ -1,5 +1,5 @@
 import logic data.prod
-using num tactic prod
+open num tactic prod
 
 inductive inh (A : Type) : Prop :=
 inh_intro : A -> inh A
@@ -30,4 +30,4 @@ theorem T1 {A B C D : Type} {P : C → Prop} (a : A) (H1 : inh B) (H2 : ∃x, P
 
 (*
 print(get_env():find("T1"):value())
-*)
\ No newline at end of file
+*)
diff --git a/tests/lean/run/class_coe.lean b/tests/lean/run/class_coe.lean
index 7feae75af..bcdf5e155 100644
--- a/tests/lean/run/class_coe.lean
+++ b/tests/lean/run/class_coe.lean
@@ -1,5 +1,5 @@
 import data.num
-using num
+open num
 
 variables int nat real : Type.{1}
 variable nat_add  : nat → nat → nat
diff --git a/tests/lean/run/coercion_bug.lean b/tests/lean/run/coercion_bug.lean
index 5281732c9..0dd664e22 100644
--- a/tests/lean/run/coercion_bug.lean
+++ b/tests/lean/run/coercion_bug.lean
@@ -1,5 +1,5 @@
 import data.nat
-using nat
+open nat
 
 definition tst1  : Prop := zero = 0
 definition tst2  : nat  := 0
diff --git a/tests/lean/run/coercion_bug2.lean b/tests/lean/run/coercion_bug2.lean
index ff61c0186..d350ff743 100644
--- a/tests/lean/run/coercion_bug2.lean
+++ b/tests/lean/run/coercion_bug2.lean
@@ -1,5 +1,5 @@
 import data.nat
-using nat
+open nat
 
 inductive list (T : Type) : Type :=
 nil {} : list T,
diff --git a/tests/lean/run/congr_imp_bug.lean b/tests/lean/run/congr_imp_bug.lean
index 8e054488b..0c6c9322e 100644
--- a/tests/lean/run/congr_imp_bug.lean
+++ b/tests/lean/run/congr_imp_bug.lean
@@ -4,7 +4,7 @@
 --- Author: Jeremy Avigad
 ----------------------------------------------------------------------------------------------------
 import logic.core.connectives struc.function
-using function
+open function
 
 namespace congr
 
diff --git a/tests/lean/run/decidable.lean b/tests/lean/run/decidable.lean
index 65bf94687..2373d80cc 100644
--- a/tests/lean/run/decidable.lean
+++ b/tests/lean/run/decidable.lean
@@ -1,5 +1,5 @@
 import logic data.unit
-using bool unit decidable
+open bool unit decidable
 
 variables a b c : bool
 variables u v : unit
diff --git a/tests/lean/run/e10.lean b/tests/lean/run/e10.lean
index ca60d98bc..5a324f3db 100644
--- a/tests/lean/run/e10.lean
+++ b/tests/lean/run/e10.lean
@@ -1,4 +1,3 @@
-
 precedence `+`:65
 
 namespace nat
@@ -8,7 +7,7 @@ namespace nat
 end nat
 
 namespace int
-  using nat (nat)
+  open nat (nat)
   variable int : Type.{1}
   variable add : int → int → int
   infixl + := add
@@ -17,8 +16,8 @@ namespace int
 end int
 
 section
-  using nat
-  using int
+  open nat
+  open int
 
   variables n m : nat
   variables i j : int
@@ -36,7 +35,7 @@ section
 
   -- Moving 'nat' to the 'front'
   print ">>> Moving nat notation to the 'front'"
-  using nat
+  open nat
   print raw i + n
   check n + m
 end
diff --git a/tests/lean/run/e11.lean b/tests/lean/run/e11.lean
index a36e48afe..d3e29926c 100644
--- a/tests/lean/run/e11.lean
+++ b/tests/lean/run/e11.lean
@@ -7,7 +7,7 @@ namespace nat
 end nat
 
 namespace int
-  using nat (nat)
+  open nat (nat)
   variable int : Type.{1}
   variable add : int → int → int
   infixl + := add
@@ -16,18 +16,18 @@ namespace int
 end int
 
 section
-  -- Using "only" the notation and declarations from the namespaces nat and int
-  using [notation] nat
-  using [notation] int
-  using [decls] nat
-  using [decls] int
+  -- Open "only" the notation and declarations from the namespaces nat and int
+  open [notation] nat
+  open [notation] int
+  open [decls] nat
+  open [decls] int
 
   variables n m : nat
   variables i j : int
   check n + m
   check i + j
 
-  -- The following check does not work, since we are not using the coercions
+  -- The following check does not work, since we are not open the coercions
   -- check n + i
 
   -- Here is a possible trick for this kind of configuration
diff --git a/tests/lean/run/e12.lean b/tests/lean/run/e12.lean
index 1644c8fc8..33106d30f 100644
--- a/tests/lean/run/e12.lean
+++ b/tests/lean/run/e12.lean
@@ -7,7 +7,7 @@ namespace nat
 end nat
 
 namespace int
-  using nat (nat)
+  open nat (nat)
   variable int : Type.{1}
   variable add : int → int → int
   infixl + := add
@@ -19,17 +19,17 @@ variables n m : nat.nat
 variables i j : int.int
 
 section
-  using [notation] nat
-  using [notation] int
-  using [decls] nat
-  using [decls] int
+  open [notation] nat
+  open [notation] int
+  open [decls] nat
+  open [decls] int
   check n+m
   check i+j
   --  check i+n -- Error
 end
 
 namespace int
-  using [decls] nat (nat)
+  open [decls] nat (nat)
   -- Here is a possible trick for this kind of configuration
   definition add_ni (a : nat) (b : int) := (of_nat a) + b
   definition add_in (a : int) (b : nat) := a + (of_nat b)
@@ -38,18 +38,18 @@ namespace int
 end int
 
 section
-  using [notation] nat
-  using [notation] int
-  using [declarations] nat
-  using [declarations] int
+  open [notation] nat
+  open [notation] int
+  open [declarations] nat
+  open [declarations] int
   check n+m
   check i+n
   check n+i
 end
 
 section
-  using nat
-  using int
+  open nat
+  open int
   check n+m
   check i+n
-end
\ No newline at end of file
+end
diff --git a/tests/lean/run/e13.lean b/tests/lean/run/e13.lean
index 112d22e60..cfa00463f 100644
--- a/tests/lean/run/e13.lean
+++ b/tests/lean/run/e13.lean
@@ -7,7 +7,7 @@ namespace nat
 end nat
 
 namespace int
-  using nat (nat)
+  open nat (nat)
   variable int : Type.{1}
   variable add : int → int → int
   infixl + := add
@@ -17,10 +17,9 @@ namespace int
   end coercions
 end int
 
-using nat
-using int
+open nat
+open int
 variables n m : nat
 check n+m -- coercion nat -> int is not available
-using int.coercions
+open int.coercions
 check n+m -- coercion nat -> int is available
-
diff --git a/tests/lean/run/e6.lean b/tests/lean/run/e6.lean
index 0ad12ebe6..a990e04d2 100644
--- a/tests/lean/run/e6.lean
+++ b/tests/lean/run/e6.lean
@@ -1,4 +1,3 @@
-
 precedence `+`:65
 
 namespace nat
@@ -8,7 +7,7 @@ namespace nat
 end nat
 
 namespace int
-  using nat (nat)
+  open nat (nat)
   variable int : Type.{1}
   variable add : int → int → int
   infixl + := add
@@ -16,8 +15,8 @@ namespace int
   coercion of_nat
 end int
 
-using int
-using nat
+open int
+open nat
 
 variables n m : nat
 variables i j : int
@@ -29,5 +28,3 @@ check i + n + n + n + n + n + n + n + n + n + n + n +
       n + n + n + n + n + n + n + n + n + n + n + n +
       n + n + n + n + n + n + n + n + n + n + n + n +
       n + n + n + n + n + n + n + n + n + n + n + n
-
-
diff --git a/tests/lean/run/e7.lean b/tests/lean/run/e7.lean
index 5ea4f59fc..042d4f995 100644
--- a/tests/lean/run/e7.lean
+++ b/tests/lean/run/e7.lean
@@ -1,4 +1,3 @@
-
 precedence `+`:65
 
 namespace nat
@@ -8,7 +7,7 @@ namespace nat
 end nat
 
 namespace int
-  using nat (nat)
+  open nat (nat)
   variable int : Type.{1}
   variable add : int → int → int
   infixl + := add
@@ -16,8 +15,8 @@ namespace int
   coercion of_nat
 end int
 
-using nat
-using int
+open nat
+open int
 
 variables n m : nat
 variables i j : int
@@ -34,6 +33,6 @@ check #nat n + m
 
 -- Moving 'nat' to the 'front'
 print ">>> Moving nat notation to the 'front'"
-using nat
+open nat
 print raw i + n
 check n + m
diff --git a/tests/lean/run/e8.lean b/tests/lean/run/e8.lean
index 914351b7d..852877e99 100644
--- a/tests/lean/run/e8.lean
+++ b/tests/lean/run/e8.lean
@@ -7,7 +7,7 @@ namespace nat
 end nat
 
 namespace int
-  using nat (nat)
+  open nat (nat)
   variable int : Type.{1}
   variable add : int → int → int
   infixl + := add
@@ -15,18 +15,18 @@ namespace int
   coercion of_nat
 end int
 
--- Using "only" the notation and declarations from the namespaces nat and int
-using [notation] nat
-using [notation] int
-using [decls] nat
-using [decls] int
+-- Open "only" the notation and declarations from the namespaces nat and int
+open [notation] nat
+open [notation] int
+open [decls] nat
+open [decls] int
 
 variables n m : nat
 variables i j : int
 check n + m
 check i + j
 
--- The following check does not work, since we are not using the coercions
+-- The following check does not work, since we are not open the coercions
 -- check n + i
 
 -- Here is a possible trick for this kind of configuration
diff --git a/tests/lean/run/e9.lean b/tests/lean/run/e9.lean
index fa45a874d..5b585020a 100644
--- a/tests/lean/run/e9.lean
+++ b/tests/lean/run/e9.lean
@@ -7,7 +7,7 @@ namespace nat
 end nat
 
 namespace int
-  using nat (nat)
+  open nat (nat)
   variable int : Type.{1}
   variable add : int → int → int
   infixl + := add
@@ -18,9 +18,9 @@ namespace int_coercions
   coercion int.of_nat
 end int_coercions
 
--- Using "only" the notation and declarations from the namespaces nat and int
-using nat
-using int
+-- Open "only" the notation and declarations from the namespaces nat and int
+open nat
+open int
 
 variables n m : nat
 variables i j : int
@@ -29,10 +29,9 @@ check i + j
 
 section
   -- Temporarily use the int_coercions
-  using int_coercions
+  open int_coercions
   check n + i
 end
 
 -- The following one is an error
 -- check n + i
-
diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean
index 4091252d6..78ebc0e45 100644
--- a/tests/lean/run/elab_bug1.lean
+++ b/tests/lean/run/elab_bug1.lean
@@ -6,7 +6,7 @@
 
 import logic struc.function
 
-using function
+open function
 
 namespace congruence
 
@@ -65,4 +65,4 @@ iff_elim_left (@congr_app _ _ R iff P C a b H) H1
 theorem test2 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
 subst_iff H1 H2
 
-end congruence
\ No newline at end of file
+end congruence
diff --git a/tests/lean/run/elim.lean b/tests/lean/run/elim.lean
index 06630a6d6..c20b5d83d 100644
--- a/tests/lean/run/elim.lean
+++ b/tests/lean/run/elim.lean
@@ -1,5 +1,5 @@
 import logic
-using num
+open num
 variable p : num → num → num → Prop
 axiom H1 : ∃ x y z, p x y z
 axiom H2 : ∀ {x y z : num}, p x y z → p x x x
diff --git a/tests/lean/run/elim2.lean b/tests/lean/run/elim2.lean
index ec19115ac..351d31dc6 100644
--- a/tests/lean/run/elim2.lean
+++ b/tests/lean/run/elim2.lean
@@ -1,5 +1,5 @@
 import logic
-using num tactic
+open num tactic
 variable p : num → num → num → Prop
 axiom H1 : ∃ x y z, p x y z
 axiom H2 : ∀ {x y z : num}, p x y z → p x x x
diff --git a/tests/lean/run/full.lean b/tests/lean/run/full.lean
index 38b48fc60..0ee5e64a1 100644
--- a/tests/lean/run/full.lean
+++ b/tests/lean/run/full.lean
@@ -2,8 +2,8 @@ import logic
 namespace foo
   variable x : num.num
   check x
-  using num
+  open num
   check x
   set_option pp.full_names true
   check x
-end foo
\ No newline at end of file
+end foo
diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean
index 6e25d91af..3eabd935f 100644
--- a/tests/lean/run/fun.lean
+++ b/tests/lean/run/fun.lean
@@ -1,5 +1,5 @@
 import logic struc.function
-using function num bool
+open function num bool
 
 
 variable f : num → bool
diff --git a/tests/lean/run/goal.lean b/tests/lean/run/goal.lean
index 2f5b49de1..f9ed94d74 100644
--- a/tests/lean/run/goal.lean
+++ b/tests/lean/run/goal.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 theorem T {a b c d : Prop} (H : a) (H : b) (H : c) (H : d) : a
-:= by state; assumption
\ No newline at end of file
+:= by state; assumption
diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean
index fb16ac892..07951788c 100644
--- a/tests/lean/run/group.lean
+++ b/tests/lean/run/group.lean
@@ -1,5 +1,5 @@
 import logic
-using num
+open num
 
 section
   parameter {A  : Type}
diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean
index ef07a783c..f56be8b4f 100644
--- a/tests/lean/run/group2.lean
+++ b/tests/lean/run/group2.lean
@@ -1,5 +1,5 @@
 import logic
-using num
+open num
 
 section
   parameter {A  : Type}
diff --git a/tests/lean/run/have5.lean b/tests/lean/run/have5.lean
index 3cd9bcead..4120df3b9 100644
--- a/tests/lean/run/have5.lean
+++ b/tests/lean/run/have5.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 variables a b c d : Prop
 axiom Ha : a
 axiom Hb : b
@@ -9,4 +9,4 @@ print raw
   then have H2 : b, by assumption,
   have H3 : c, by assumption,
   then have H4 : d, by assumption,
-  H4
\ No newline at end of file
+  H4
diff --git a/tests/lean/run/is_nil.lean b/tests/lean/run/is_nil.lean
index dfa0355e7..695879842 100644
--- a/tests/lean/run/is_nil.lean
+++ b/tests/lean/run/is_nil.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 inductive list (A : Type) : Type :=
 nil {} : list A,
diff --git a/tests/lean/run/list_elab1.lean b/tests/lean/run/list_elab1.lean
index 47f71cd8b..6389506e0 100644
--- a/tests/lean/run/list_elab1.lean
+++ b/tests/lean/run/list_elab1.lean
@@ -10,7 +10,7 @@
 -- Basic properties of lists.
 
 import data.nat
-using nat eq_ops
+open nat eq_ops
 inductive list (T : Type) : Type :=
 nil {} : list T,
 cons : T → list T → list T
diff --git a/tests/lean/run/local_using.lean b/tests/lean/run/local_using.lean
index 3ad955dd7..a9412c70d 100644
--- a/tests/lean/run/local_using.lean
+++ b/tests/lean/run/local_using.lean
@@ -15,10 +15,8 @@ end bla
 
 variable g : N → N → N
 
-using foo
-using bla
+open foo
+open bla
 print raw a + b -- + is overloaded, it creates a choice
 print raw #foo a + b   -- + is not overloaded, we are parsing inside #foo
 print raw g (#foo a + b) (#bla a + b) -- mixing both
-
-
diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean
index bc1f66753..ff1110a11 100644
--- a/tests/lean/run/match1.lean
+++ b/tests/lean/run/match1.lean
@@ -1,5 +1,5 @@
 import data.nat
-using nat
+open nat
 
 definition two1 : nat := 2
 definition two2 : nat := succ (succ (zero))
diff --git a/tests/lean/run/match2.lean b/tests/lean/run/match2.lean
index de86bb114..2bd457fd1 100644
--- a/tests/lean/run/match2.lean
+++ b/tests/lean/run/match2.lean
@@ -1,5 +1,5 @@
 import data.nat
-using nat
+open nat
 
 definition two1 : nat := 2
 definition two2 : nat := succ (succ (zero))
diff --git a/tests/lean/run/nat_bug.lean b/tests/lean/run/nat_bug.lean
index ba055e69c..5716c3613 100644
--- a/tests/lean/run/nat_bug.lean
+++ b/tests/lean/run/nat_bug.lean
@@ -1,5 +1,5 @@
 import logic
-using decidable
+open decidable
 
 inductive nat : Type :=
 zero : nat,
diff --git a/tests/lean/run/nat_bug2.lean b/tests/lean/run/nat_bug2.lean
index fe33dad2d..456c6da7a 100644
--- a/tests/lean/run/nat_bug2.lean
+++ b/tests/lean/run/nat_bug2.lean
@@ -1,5 +1,5 @@
 import logic
-using num eq_ops
+open num eq_ops
 
 inductive nat : Type :=
 zero : nat,
diff --git a/tests/lean/run/nat_bug3.lean b/tests/lean/run/nat_bug3.lean
index a57260055..0282d8d82 100644
--- a/tests/lean/run/nat_bug3.lean
+++ b/tests/lean/run/nat_bug3.lean
@@ -1,5 +1,5 @@
 import logic
-using num eq_ops
+open num eq_ops
 
 inductive nat : Type :=
 zero : nat,
diff --git a/tests/lean/run/nat_bug4.lean b/tests/lean/run/nat_bug4.lean
index 10f198248..9a94a2cfa 100644
--- a/tests/lean/run/nat_bug4.lean
+++ b/tests/lean/run/nat_bug4.lean
@@ -1,5 +1,5 @@
 import logic
-using num eq_ops
+open num eq_ops
 
 inductive nat : Type :=
 zero : nat,
diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean
index 84c90e7cb..e172cc3d8 100644
--- a/tests/lean/run/nat_bug5.lean
+++ b/tests/lean/run/nat_bug5.lean
@@ -1,5 +1,5 @@
 import logic
-using num eq_ops
+open num eq_ops
 
 inductive nat : Type :=
 zero : nat,
diff --git a/tests/lean/run/nat_bug6.lean b/tests/lean/run/nat_bug6.lean
index ba9e08193..9be8a1ffc 100644
--- a/tests/lean/run/nat_bug6.lean
+++ b/tests/lean/run/nat_bug6.lean
@@ -1,5 +1,5 @@
 import logic
-using eq_ops
+open eq_ops
 
 inductive nat : Type :=
 zero : nat,
diff --git a/tests/lean/run/not_bug1.lean b/tests/lean/run/not_bug1.lean
index 0e02f4ed9..fdbebb13a 100644
--- a/tests/lean/run/not_bug1.lean
+++ b/tests/lean/run/not_bug1.lean
@@ -1,5 +1,5 @@
 import logic
-using bool
+open bool
 
 variable list : Type.{1}
 variable nil  : list
diff --git a/tests/lean/run/ns.lean b/tests/lean/run/ns.lean
index 1ddf45447..6be6578ac 100644
--- a/tests/lean/run/ns.lean
+++ b/tests/lean/run/ns.lean
@@ -1,5 +1,3 @@
-
-
 variable nat : Type.{1}
 variable f : nat → nat
 
@@ -12,7 +10,7 @@ namespace foo
   check f i
 end foo
 
-using foo
+open foo
 variables a : nat
 variables i : int
 check f a
diff --git a/tests/lean/run/ns1.lean b/tests/lean/run/ns1.lean
index e9915d9e4..123ca5987 100644
--- a/tests/lean/run/ns1.lean
+++ b/tests/lean/run/ns1.lean
@@ -6,5 +6,5 @@ theorem tst : true := trivial
 end boo
 end foo
 
-using foo
-check boo.tst
\ No newline at end of file
+open foo
+check boo.tst
diff --git a/tests/lean/run/occurs_check_bug1.lean b/tests/lean/run/occurs_check_bug1.lean
index 83ba9654a..656901fb3 100644
--- a/tests/lean/run/occurs_check_bug1.lean
+++ b/tests/lean/run/occurs_check_bug1.lean
@@ -1,7 +1,7 @@
 import logic data.nat data.prod
 
-using nat prod
-using decidable
+open nat prod
+open decidable
 
 variable modulo (x : ℕ) (y : ℕ) : ℕ
 infixl `mod`:70 := modulo
diff --git a/tests/lean/run/over2.lean b/tests/lean/run/over2.lean
index 525648cbe..f0f924845 100644
--- a/tests/lean/run/over2.lean
+++ b/tests/lean/run/over2.lean
@@ -1,5 +1,5 @@
 import data.nat
-using nat
+open nat
 
 namespace N1
   definition foo (a : nat) := a
@@ -9,6 +9,6 @@ namespace N2
   definition foo (a : nat) := a
 end N2
 
-using N1 N2
+open N1 N2
 
-definition boo := foo
\ No newline at end of file
+definition boo := foo
diff --git a/tests/lean/run/over_subst.lean b/tests/lean/run/over_subst.lean
index 52f49e121..6f752e6d7 100644
--- a/tests/lean/run/over_subst.lean
+++ b/tests/lean/run/over_subst.lean
@@ -24,8 +24,8 @@ abbreviation lt (a b : int) := a + one ≤ b
 infix `<`:50  := lt
 end int
 
-using int
-using nat
+open int
+open nat
 
 theorem add_lt_left {a b : int} (H : a < b) (c : int) : c + a < c + b :=
 subst (symm (add_assoc c a one)) (add_le_left H c)
diff --git a/tests/lean/run/ptst.lean b/tests/lean/run/ptst.lean
index 1e501bb4f..dd4bdb8a0 100644
--- a/tests/lean/run/ptst.lean
+++ b/tests/lean/run/ptst.lean
@@ -1,5 +1,5 @@
 import logic data.prod
-using prod
+open prod
 
 -- Test tuple notation
 check (3, false, 1, true)
diff --git a/tests/lean/run/rel.lean b/tests/lean/run/rel.lean
index b725f7ad4..8b58b0e9f 100644
--- a/tests/lean/run/rel.lean
+++ b/tests/lean/run/rel.lean
@@ -1,5 +1,5 @@
 import logic struc.relation
-using relation
+open relation
 
 namespace is_equivalence
 
diff --git a/tests/lean/run/root.lean b/tests/lean/run/root.lean
index 30dfa550f..4d1f43e28 100644
--- a/tests/lean/run/root.lean
+++ b/tests/lean/run/root.lean
@@ -1,5 +1,5 @@
 import logic
-using num
+open num
 
 variable foo : Prop
 
diff --git a/tests/lean/run/section1.lean b/tests/lean/run/section1.lean
index 2bc6619e5..f5385af27 100644
--- a/tests/lean/run/section1.lean
+++ b/tests/lean/run/section1.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 section
   set_option pp.universes true
@@ -11,4 +11,4 @@ section
   check H1
   check H
   check H2
-end
\ No newline at end of file
+end
diff --git a/tests/lean/run/set.lean b/tests/lean/run/set.lean
index f09791b80..307c97b24 100644
--- a/tests/lean/run/set.lean
+++ b/tests/lean/run/set.lean
@@ -1,7 +1,7 @@
 import logic
-using bool
+open bool
 
 definition set {{T : Type}} := T → bool
 infix `∈`:50 := λx A, A x = tt
 
-check 1 ∈ (λ x, tt)
\ No newline at end of file
+check 1 ∈ (λ x, tt)
diff --git a/tests/lean/run/set2.lean b/tests/lean/run/set2.lean
index 2bf19ce09..1af9dd800 100644
--- a/tests/lean/run/set2.lean
+++ b/tests/lean/run/set2.lean
@@ -1,5 +1,5 @@
 import logic
-using bool
+open bool
 
 namespace set
 
@@ -17,4 +17,4 @@ section
   := not_intro (λH : x ∈ ∅, absurd H ff_ne_tt)
 end
 
-end set
\ No newline at end of file
+end set
diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean
index 8800de6eb..09fbc10fb 100644
--- a/tests/lean/run/sum_bug.lean
+++ b/tests/lean/run/sum_bug.lean
@@ -4,7 +4,7 @@
 
 import logic.core.prop logic.classes.inhabited logic.classes.decidable
 
-using inhabited decidable
+open inhabited decidable
 
 namespace sum
 
diff --git a/tests/lean/run/t8.lean b/tests/lean/run/t8.lean
index 4e8821a1d..4389d315b 100644
--- a/tests/lean/run/t8.lean
+++ b/tests/lean/run/t8.lean
@@ -1,3 +1,3 @@
 import logic
-using tactic
-print raw (by assumption)
\ No newline at end of file
+open tactic
+print raw (by assumption)
diff --git a/tests/lean/run/tactic1.lean b/tests/lean/run/tactic1.lean
index 38141de19..99fedddeb 100644
--- a/tests/lean/run/tactic1.lean
+++ b/tests/lean/run/tactic1.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : A
 := by assumption
diff --git a/tests/lean/run/tactic10.lean b/tests/lean/run/tactic10.lean
index 8f9cc44b8..4724467e8 100644
--- a/tests/lean/run/tactic10.lean
+++ b/tests/lean/run/tactic10.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a
 := by apply iff_intro;
diff --git a/tests/lean/run/tactic11.lean b/tests/lean/run/tactic11.lean
index 052d7eb94..e7ec0b014 100644
--- a/tests/lean/run/tactic11.lean
+++ b/tests/lean/run/tactic11.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a
 := have H1 [fact] : a → b, -- We need to mark H1 as fact, otherwise it is not visible by tactics
diff --git a/tests/lean/run/tactic12.lean b/tests/lean/run/tactic12.lean
index 95c7e0b8d..c4ca364e2 100644
--- a/tests/lean/run/tactic12.lean
+++ b/tests/lean/run/tactic12.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b
 := by apply and_intro;
diff --git a/tests/lean/run/tactic13.lean b/tests/lean/run/tactic13.lean
index 74f423acc..034e5c727 100644
--- a/tests/lean/run/tactic13.lean
+++ b/tests/lean/run/tactic13.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b :=
 begin
diff --git a/tests/lean/run/tactic14.lean b/tests/lean/run/tactic14.lean
index 23fb1c72b..e0a9eecae 100644
--- a/tests/lean/run/tactic14.lean
+++ b/tests/lean/run/tactic14.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 definition basic_tac : tactic
 := repeat [apply @and_intro | assumption]
diff --git a/tests/lean/run/tactic15.lean b/tests/lean/run/tactic15.lean
index da5146924..30be170f8 100644
--- a/tests/lean/run/tactic15.lean
+++ b/tests/lean/run/tactic15.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 variable A : Type.{1}
 variable f : A → A → A
diff --git a/tests/lean/run/tactic16.lean b/tests/lean/run/tactic16.lean
index effced0e1..a56c49102 100644
--- a/tests/lean/run/tactic16.lean
+++ b/tests/lean/run/tactic16.lean
@@ -1,5 +1,5 @@
 import logic data.string
-using tactic
+open tactic
 
 variable A : Type.{1}
 variable f : A → A → A
diff --git a/tests/lean/run/tactic17.lean b/tests/lean/run/tactic17.lean
index de3360d1f..19b04185a 100644
--- a/tests/lean/run/tactic17.lean
+++ b/tests/lean/run/tactic17.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 variable A : Type.{1}
 variable f : A → A → A
diff --git a/tests/lean/run/tactic18.lean b/tests/lean/run/tactic18.lean
index 9a52c9211..d5f7468ab 100644
--- a/tests/lean/run/tactic18.lean
+++ b/tests/lean/run/tactic18.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 variable A : Type.{1}
 variable f : A → A → A
diff --git a/tests/lean/run/tactic19.lean b/tests/lean/run/tactic19.lean
index 87d7912a0..aaaf7013a 100644
--- a/tests/lean/run/tactic19.lean
+++ b/tests/lean/run/tactic19.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 theorem tst {A : Type} {f : A → A → A} {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c
 := by apply congr;
diff --git a/tests/lean/run/tactic2.lean b/tests/lean/run/tactic2.lean
index 9b378296b..fc8664d68 100644
--- a/tests/lean/run/tactic2.lean
+++ b/tests/lean/run/tactic2.lean
@@ -1,7 +1,7 @@
 import logic
-using tactic
+open tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : A
 := by state; assumption
 
-check tst
\ No newline at end of file
+check tst
diff --git a/tests/lean/run/tactic20.lean b/tests/lean/run/tactic20.lean
index addbb6a28..841186539 100644
--- a/tests/lean/run/tactic20.lean
+++ b/tests/lean/run/tactic20.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 definition assump := eassumption
 
diff --git a/tests/lean/run/tactic21.lean b/tests/lean/run/tactic21.lean
index eac4b7b1d..09868af7d 100644
--- a/tests/lean/run/tactic21.lean
+++ b/tests/lean/run/tactic21.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 definition assump := eassumption
 
diff --git a/tests/lean/run/tactic22.lean b/tests/lean/run/tactic22.lean
index 6625af12c..72d529a45 100644
--- a/tests/lean/run/tactic22.lean
+++ b/tests/lean/run/tactic22.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 theorem T (a b c d : Prop) (Ha : a) (Hb : b) (Hc : c) (Hd : d) : a ∧ b ∧ c ∧ d
 := by fixpoint (λ f, [apply @and_intro; f | assumption; f | id])
diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean
index 49430daf2..e4064b382 100644
--- a/tests/lean/run/tactic23.lean
+++ b/tests/lean/run/tactic23.lean
@@ -1,6 +1,6 @@
 import logic
-using num (num pos_num num_rec pos_num_rec)
-using tactic
+open num (num pos_num num_rec pos_num_rec)
+open tactic
 
 inductive nat : Type :=
 zero : nat,
diff --git a/tests/lean/run/tactic24.lean b/tests/lean/run/tactic24.lean
index d85d7aceb..91de99bd3 100644
--- a/tests/lean/run/tactic24.lean
+++ b/tests/lean/run/tactic24.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 definition my_tac1 := apply @refl
 definition my_tac2 := repeat (apply @and_intro; assumption)
diff --git a/tests/lean/run/tactic25.lean b/tests/lean/run/tactic25.lean
index 8c9ccbad6..39d86f45a 100644
--- a/tests/lean/run/tactic25.lean
+++ b/tests/lean/run/tactic25.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 definition my_tac1 := apply @refl
 definition my_tac2 := repeat (apply @and_intro; assumption)
diff --git a/tests/lean/run/tactic26.lean b/tests/lean/run/tactic26.lean
index 563cfa9a0..3ecad8464 100644
--- a/tests/lean/run/tactic26.lean
+++ b/tests/lean/run/tactic26.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic inhabited
+open tactic inhabited
 
 inductive sum (A : Type) (B : Type) : Type :=
 inl  : A → sum A B,
diff --git a/tests/lean/run/tactic27.lean b/tests/lean/run/tactic27.lean
index fd74f1e3b..64a635017 100644
--- a/tests/lean/run/tactic27.lean
+++ b/tests/lean/run/tactic27.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 definition my_tac := repeat ([ apply @and_intro
                              | apply @refl
diff --git a/tests/lean/run/tactic28.lean b/tests/lean/run/tactic28.lean
index f5f3f1571..2f29c2551 100644
--- a/tests/lean/run/tactic28.lean
+++ b/tests/lean/run/tactic28.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic inhabited
+open tactic inhabited
 
 inductive sum (A : Type) (B : Type) : Type :=
 inl  : A → sum A B,
diff --git a/tests/lean/run/tactic29.lean b/tests/lean/run/tactic29.lean
index d6584770b..7c54d4879 100644
--- a/tests/lean/run/tactic29.lean
+++ b/tests/lean/run/tactic29.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 section
   set_option pp.universes true
@@ -15,4 +15,4 @@ section
   := by apply and_intro; apply H; apply refl
 end
 
-check @test
\ No newline at end of file
+check @test
diff --git a/tests/lean/run/tactic3.lean b/tests/lean/run/tactic3.lean
index 781e8d773..6ecc69c03 100644
--- a/tests/lean/run/tactic3.lean
+++ b/tests/lean/run/tactic3.lean
@@ -1,9 +1,9 @@
 import logic
-using tactic
+open tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : A
 := by [trace "first";  state; now  |
        trace "second"; state; fail |
        trace "third";  assumption]
 
-check tst
\ No newline at end of file
+check tst
diff --git a/tests/lean/run/tactic30.lean b/tests/lean/run/tactic30.lean
index ce59a9db7..77e93a9ee 100644
--- a/tests/lean/run/tactic30.lean
+++ b/tests/lean/run/tactic30.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 section
   set_option pp.universes true
@@ -11,4 +11,4 @@ section
   := including H, by apply and_intro; assumption; apply refl
 end
 
-check @test
\ No newline at end of file
+check @test
diff --git a/tests/lean/run/tactic4.lean b/tests/lean/run/tactic4.lean
index 9eb19bb9c..25212b0b5 100644
--- a/tests/lean/run/tactic4.lean
+++ b/tests/lean/run/tactic4.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic (renaming id->id_tac)
+open tactic (renaming id->id_tac)
 
 definition id {A : Type} (a : A) := a
 
diff --git a/tests/lean/run/tactic5.lean b/tests/lean/run/tactic5.lean
index c25c006b0..9f7264782 100644
--- a/tests/lean/run/tactic5.lean
+++ b/tests/lean/run/tactic5.lean
@@ -1,9 +1,9 @@
 import logic
-using tactic (renaming id->id_tac)
+open tactic (renaming id->id_tac)
 
 definition id {A : Type} (a : A) := a
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : id A
 := by !(unfold @id; state); assumption
 
-check tst
\ No newline at end of file
+check tst
diff --git a/tests/lean/run/tactic6.lean b/tests/lean/run/tactic6.lean
index fa04b08c5..e5a3a39e1 100644
--- a/tests/lean/run/tactic6.lean
+++ b/tests/lean/run/tactic6.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic (renaming id->id_tac)
+open tactic (renaming id->id_tac)
 
 definition id {A : Type} (a : A) := a
 
diff --git a/tests/lean/run/tactic7.lean b/tests/lean/run/tactic7.lean
index afddec6e1..b9a378a81 100644
--- a/tests/lean/run/tactic7.lean
+++ b/tests/lean/run/tactic7.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A
 := by apply and_intro; state; assumption; apply and_intro; !assumption
diff --git a/tests/lean/run/tactic8.lean b/tests/lean/run/tactic8.lean
index 812d12eae..8a6d14379 100644
--- a/tests/lean/run/tactic8.lean
+++ b/tests/lean/run/tactic8.lean
@@ -1,9 +1,9 @@
 import logic
-using tactic
+open tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A
 := by (apply @and_intro;
        apply (show A, from H1);
        apply (show B ∧ A, from and_intro H2 H1))
 
-check @tst
\ No newline at end of file
+check @tst
diff --git a/tests/lean/run/tactic9.lean b/tests/lean/run/tactic9.lean
index c90e2f76e..f9d0c2fc2 100644
--- a/tests/lean/run/tactic9.lean
+++ b/tests/lean/run/tactic9.lean
@@ -1,5 +1,5 @@
 import logic
-using tactic
+open tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : ((fun x : Prop, x) A) ∧ B ∧ A
 := by apply and_intro; beta; assumption; apply and_intro; !assumption
diff --git a/tests/lean/run/trick.lean b/tests/lean/run/trick.lean
index b7545399d..aaa7cc379 100644
--- a/tests/lean/run/trick.lean
+++ b/tests/lean/run/trick.lean
@@ -1,5 +1,5 @@
 import logic
-using num
+open num
 
 definition proj1 (x : num) (y : num) := x
 definition One := 1
diff --git a/tests/lean/run/univ_bug1.lean b/tests/lean/run/univ_bug1.lean
index 6f1dcac43..a0053cb7f 100644
--- a/tests/lean/run/univ_bug1.lean
+++ b/tests/lean/run/univ_bug1.lean
@@ -5,7 +5,7 @@
 ----------------------------------------------------------------------------------------------------
 
 import logic data.nat
-using nat
+open nat
 
 namespace simp
 -- set_option pp.universes true
@@ -25,4 +25,4 @@ theorem simp_app [instance] (S T : Type) (f1 f2 : S → T) (s1 s2 : S)
    (C1 : simplifies_to f1 f2) (C2 : simplifies_to s1 s2) : simplifies_to (f1 s1) (f2 s2) :=
 mk (congr (get_eq C1) (get_eq C2))
 
-end simp
\ No newline at end of file
+end simp
diff --git a/tests/lean/run/univ_bug2.lean b/tests/lean/run/univ_bug2.lean
index cd3885e3d..ad3c6833f 100644
--- a/tests/lean/run/univ_bug2.lean
+++ b/tests/lean/run/univ_bug2.lean
@@ -5,7 +5,7 @@
 ----------------------------------------------------------------------------------------------------
 
 import logic data.nat
-using nat
+open nat
 
 namespace simp
 -- first define a class of homogeneous equality
@@ -28,4 +28,4 @@ have Rs [fact] : simplifies_to f1 f2, from mk Hf,
 have Cs [fact] : simplifies_to s1 s2, from mk Hs,
 infer_eq _ _
 
-end simp
\ No newline at end of file
+end simp
diff --git a/tests/lean/show1.lean b/tests/lean/show1.lean
index 36f9ef7e1..fe3147b2f 100644
--- a/tests/lean/show1.lean
+++ b/tests/lean/show1.lean
@@ -1,5 +1,5 @@
 import logic
-using bool eq_ops tactic
+open bool eq_ops tactic
 
 variables a b c : bool
 axiom H1 : a = b
diff --git a/tests/lean/slow/list_elab2.lean b/tests/lean/slow/list_elab2.lean
index 16230f1ea..1315debd8 100644
--- a/tests/lean/slow/list_elab2.lean
+++ b/tests/lean/slow/list_elab2.lean
@@ -12,9 +12,9 @@
 import logic data.nat
 -- import congr
 
-using nat
--- using congr
-using eq_ops
+open nat
+-- open congr
+open eq_ops
 
 namespace list
 
diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean
index 056d58f5d..3a4139636 100644
--- a/tests/lean/slow/nat_wo_hints.lean
+++ b/tests/lean/slow/nat_wo_hints.lean
@@ -4,8 +4,8 @@
 -- Author: Floris van Doorn
 ----------------------------------------------------------------------------------------------------
 import logic struc.binary
-using tactic num binary eq_ops
-using decidable
+open tactic num binary eq_ops
+open decidable
 
 namespace nat
 inductive nat : Type :=
@@ -24,7 +24,7 @@ namespace helper_tactics
   definition apply_refl := apply @refl
   tactic_hint apply_refl
 end helper_tactics
-using helper_tactics
+open helper_tactics
 
 theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat_rec x f 0 = x
 
diff --git a/tests/lean/slow/path_groupoids.lean b/tests/lean/slow/path_groupoids.lean
index 6aa5e7eb5..2a5fed8e9 100644
--- a/tests/lean/slow/path_groupoids.lean
+++ b/tests/lean/slow/path_groupoids.lean
@@ -27,7 +27,7 @@ namespace path
   path_rec H p
 end path
 
-using path
+open path
 
 -- Concatenation and inverse
 -- -------------------------
diff --git a/tests/lean/t14.lean b/tests/lean/t14.lean
index df567dfce..a21361231 100644
--- a/tests/lean/t14.lean
+++ b/tests/lean/t14.lean
@@ -6,25 +6,25 @@ namespace foo
 end foo
 
 context
-  using foo (renaming a->b x->y) (hiding c)
+  open foo (renaming a->b x->y) (hiding c)
   check b
   check y
   check c -- Error
 end
 
 context
-  using foo (a x)
+  open foo (a x)
   check a
   check x
   check c -- Error
 end
 
 context
-  using foo (a x) (hiding c) -- Error
+  open foo (a x) (hiding c) -- Error
 end
 
 context
-  using foo
+  open foo
   check a
   check c
   check A
@@ -36,18 +36,18 @@ namespace foo
 end foo
 
 context
-  using foo
+  open foo
   check a * c
 end
 
 context
-  using [notation] foo -- use only the notation
+  open [notation] foo -- use only the notation
   check foo.a * foo.c
   check a * c -- Error
 end
 
 context
-  using [decls] foo -- use only the declarations
+  open [decls] foo -- use only the declarations
   check f a c
   check a*c -- Error
 end
diff --git a/tests/lean/t14.lean.expected.out b/tests/lean/t14.lean.expected.out
index f3eeeadf0..5178e571e 100644
--- a/tests/lean/t14.lean.expected.out
+++ b/tests/lean/t14.lean.expected.out
@@ -4,7 +4,7 @@ t14.lean:12:8: error: unknown identifier 'c'
 a : foo.A
 x : foo.A
 t14.lean:19:8: error: unknown identifier 'c'
-t14.lean:23:27: error: invalid 'using' command option, mixing explicit and implicit 'using' options
+t14.lean:23:26: error: invalid 'open' command option, mixing explicit and implicit 'open' options
 a : A
 c : A
 A : Type
diff --git a/tests/lean/uni_bug1.lean b/tests/lean/uni_bug1.lean
index a5558a74a..643e370b7 100644
--- a/tests/lean/uni_bug1.lean
+++ b/tests/lean/uni_bug1.lean
@@ -1,5 +1,5 @@
 import data.nat data.prod
-using nat prod
+open nat prod
 
 variable R : nat → nat → Prop
 variable f (a b : nat) (H : R a b) : nat