diff --git a/library/data/lazy_list.lean b/library/data/lazy_list.lean
index ef1e5d1c06..2f98efca32 100644
--- a/library/data/lazy_list.lean
+++ b/library/data/lazy_list.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-universe variables u v w
+universes u v w
 
 inductive lazy_list (α : Type u) : Type u
 | nil {} : lazy_list
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index a97e097329..b1bfd66181 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -7,7 +7,7 @@ Basic properties of lists.
 -/
 import init.data.list.basic
 
-universe variables u v w
+universes u v w
 
 namespace list
 
diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean
index a2d1ee6ad9..a9b01f6dc9 100644
--- a/library/data/list/comb.lean
+++ b/library/data/list/comb.lean
@@ -7,7 +7,7 @@ List combinators.
 -/
 import init.data.list.basic
 
-universe variables u v w
+universes u v w
 
 namespace list
 
diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean
index 4fab1bbcfe..d27b4c3271 100644
--- a/library/data/set/basic.lean
+++ b/library/data/set/basic.lean
@@ -3,9 +3,8 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad, Leonardo de Moura
 -/
-
 namespace set
-universe variable u
+universes u
 variable {α : Type u}
 
 lemma ext {a b : set α} (h : ∀ x, x ∈ a ↔ x ∈ b) : a = b :=
diff --git a/library/data/stream.lean b/library/data/stream.lean
index e1fc1ae6bc..59bfae1e49 100644
--- a/library/data/stream.lean
+++ b/library/data/stream.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 open nat function option
-universe variables u v w
+universes u v w
 
 def stream (α : Type u) := nat → α
 
diff --git a/library/data/vector.lean b/library/data/vector.lean
index d26e43c993..d09a98260a 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -8,7 +8,7 @@ It is implemented as a subtype.
 -/
 import data.list
 
-universe variables u v w
+universes u v w
 
 def vector (α : Type u) (n : ℕ) := { l : list α // l^.length = n }
 
diff --git a/library/init/algebra/ac.lean b/library/init/algebra/ac.lean
index 76c644b449..5da51c6f45 100644
--- a/library/init/algebra/ac.lean
+++ b/library/init/algebra/ac.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.logic
-universe variables u
+universe u
 
 class is_associative (α : Type u) (op : α → α → α) :=
 (assoc : ∀ a b c, op (op a b) c = op a (op b c))
diff --git a/library/init/algebra/field.lean b/library/init/algebra/field.lean
index 20c062c2a1..eb1dd758bb 100644
--- a/library/init/algebra/field.lean
+++ b/library/init/algebra/field.lean
@@ -8,7 +8,7 @@ The development is modeled after Isabelle's library.
 -/
 prelude
 import init.algebra.ring
-universe variables u
+universe u
 
 /- Make sure instances defined in this file have lower priority than the ones
    defined for concrete structures -/
diff --git a/library/init/algebra/functions.lean b/library/init/algebra/functions.lean
index 36843005ce..26906410f0 100644
--- a/library/init/algebra/functions.lean
+++ b/library/init/algebra/functions.lean
@@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
 prelude
 import init.algebra.ordered_field
 
-universe variables u
+universe u
 
 definition min {α : Type u} [decidable_linear_order α] (a b : α) : α := if a ≤ b then a else b
 definition max {α : Type u} [decidable_linear_order α] (a b : α) : α := if a ≤ b then b else a
diff --git a/library/init/algebra/group.lean b/library/init/algebra/group.lean
index 008feb7a79..e603c0c5f9 100644
--- a/library/init/algebra/group.lean
+++ b/library/init/algebra/group.lean
@@ -10,7 +10,7 @@ import init.logic init.algebra.ac init.meta init.meta.decl_cmds
    defined for concrete structures -/
 set_option default_priority 100
 
-universe variable u
+universe u
 variables {α : Type u}
 
 class semigroup (α : Type u) extends has_mul α :=
diff --git a/library/init/algebra/norm_num.lean b/library/init/algebra/norm_num.lean
index 74ead18775..6178520748 100644
--- a/library/init/algebra/norm_num.lean
+++ b/library/init/algebra/norm_num.lean
@@ -7,7 +7,7 @@ prelude
 import init.algebra.field init.algebra.ordered_ring
 
 namespace norm_num
-universe variable u
+universe u
 variable {α : Type u}
 
 def add1 [has_add α] [has_one α] (a : α) : α :=
diff --git a/library/init/algebra/order.lean b/library/init/algebra/order.lean
index 0ba02f9998..2680628c2b 100644
--- a/library/init/algebra/order.lean
+++ b/library/init/algebra/order.lean
@@ -9,7 +9,7 @@ import init.logic
    defined for concrete structures -/
 set_option default_priority 100
 
-universe variable u
+universe u
 variables {α : Type u}
 
 class weak_order (α : Type u) extends has_le α :=
diff --git a/library/init/algebra/ordered_field.lean b/library/init/algebra/ordered_field.lean
index c5ea4dc83e..9de7c289c1 100644
--- a/library/init/algebra/ordered_field.lean
+++ b/library/init/algebra/ordered_field.lean
@@ -6,7 +6,7 @@ Authors: Robert Lewis, Leonardo de Moura
 prelude
 import init.algebra.ordered_ring init.algebra.field
 
-universe variables u
+universe u
 
 class linear_ordered_field (α : Type u) extends linear_ordered_ring α, field α
 
diff --git a/library/init/algebra/ordered_group.lean b/library/init/algebra/ordered_group.lean
index 207acd2577..52b4a75acf 100644
--- a/library/init/algebra/ordered_group.lean
+++ b/library/init/algebra/ordered_group.lean
@@ -10,7 +10,7 @@ import init.algebra.order init.algebra.group
    defined for concrete structures -/
 set_option default_priority 100
 
-universe variable u
+universe u
 
 class ordered_cancel_comm_monoid (α : Type u)
       extends add_comm_monoid α, add_left_cancel_semigroup α,
diff --git a/library/init/algebra/ordered_ring.lean b/library/init/algebra/ordered_ring.lean
index 59680a5634..875929a0ee 100644
--- a/library/init/algebra/ordered_ring.lean
+++ b/library/init/algebra/ordered_ring.lean
@@ -10,7 +10,7 @@ import init.algebra.ordered_group init.algebra.ring
    defined for concrete structures -/
 set_option default_priority 100
 
-universe variable u
+universe u
 
 class ordered_semiring (α : Type u)
   extends semiring α, ordered_cancel_comm_monoid α :=
diff --git a/library/init/algebra/ring.lean b/library/init/algebra/ring.lean
index 998b7f1580..ab1d561c0a 100644
--- a/library/init/algebra/ring.lean
+++ b/library/init/algebra/ring.lean
@@ -10,7 +10,7 @@ import init.algebra.group
    defined for concrete structures -/
 set_option default_priority 100
 
-universe variable u
+universe u
 
 class distrib (α : Type u) extends has_mul α, has_add α :=
 (left_distrib : ∀ a b c : α, a * (b + c) = (a * b) + (a * c))
diff --git a/library/init/category/alternative.lean b/library/init/category/alternative.lean
index c63686e071..bd0a3d4aae 100644
--- a/library/init/category/alternative.lean
+++ b/library/init/category/alternative.lean
@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.logic init.category.applicative
-universe variables u v
+universes u v
 
 class alternative (f : Type u → Type v) extends applicative f : Type (max u+1 v) :=
 (failure : Π {a : Type u}, f a)
diff --git a/library/init/category/applicative.lean b/library/init/category/applicative.lean
index 474da30199..1c842491dd 100644
--- a/library/init/category/applicative.lean
+++ b/library/init/category/applicative.lean
@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.category.functor
-universe variables u v
+universes u v
 
 class applicative (f : Type u → Type v) extends functor f : Type (max u+1 v):=
 (pure : Π {a : Type u}, a → f a)
diff --git a/library/init/category/combinators.lean b/library/init/category/combinators.lean
index 29aa1334d2..a3f747ad68 100644
--- a/library/init/category/combinators.lean
+++ b/library/init/category/combinators.lean
@@ -7,7 +7,7 @@ Monad combinators, as in Haskell's Control.Monad.
 -/
 prelude
 import init.category.monad init.data.list.basic
-universe variables u v w
+universes u v w
 
 namespace monad
 def mapm {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (f : α → m β) : list α → m (list β)
diff --git a/library/init/category/functor.lean b/library/init/category/functor.lean
index bf01004df7..292c2e1f22 100644
--- a/library/init/category/functor.lean
+++ b/library/init/category/functor.lean
@@ -5,7 +5,7 @@ Authors: Luke Nelson and Jared Roesch
 -/
 prelude
 import init.core
-universe variables u v
+universes u v
 
 class functor (f : Type u → Type v) : Type (max u+1 v) :=
 (map : Π {a b : Type u}, (a → b) → f a → f b)
diff --git a/library/init/category/monad.lean b/library/init/category/monad.lean
index cb7fb54437..462a1d1e86 100644
--- a/library/init/category/monad.lean
+++ b/library/init/category/monad.lean
@@ -5,7 +5,7 @@ Authors: Luke Nelson and Jared Roesch
 -/
 prelude
 import init.category.applicative
-universe variables u v
+universes u v
 
 class pre_monad (m : Type u → Type v) :=
 (bind : Π {a b : Type u}, m a → (a → m b) → m b)
diff --git a/library/init/category/monad_fail.lean b/library/init/category/monad_fail.lean
index b86df08320..4761f93517 100644
--- a/library/init/category/monad_fail.lean
+++ b/library/init/category/monad_fail.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import init.category.monad init.data.string.basic
 
-universe variables u v
+universes u v
 
 class monad_fail (m : Type u → Type v) extends monad m :=
 (fail : Π {a}, string → m a)
diff --git a/library/init/cc_lemmas.lean b/library/init/cc_lemmas.lean
index 36aefa1d31..56f3ca3edf 100644
--- a/library/init/cc_lemmas.lean
+++ b/library/init/cc_lemmas.lean
@@ -76,7 +76,7 @@ lemma false_of_a_eq_not_a {a : Prop} (h : a = not a) : false :=
 have not a, from λ ha, absurd ha (eq.mp h ha),
 absurd (eq.mpr h this) this
 
-universe variables u
+universes u
 
 lemma if_eq_of_eq_true {c : Prop} [d : decidable c] {α : Sort u} (t e : α) (h : c = true) : (@ite c d α t e) = t :=
 if_pos (of_eq_true h)
diff --git a/library/init/classical.lean b/library/init/classical.lean
index 94a558f720..8531e99b79 100644
--- a/library/init/classical.lean
+++ b/library/init/classical.lean
@@ -8,7 +8,7 @@ import init.data.subtype.basic init.funext
 open subtype
 
 namespace classical
-universe variables u v
+universes u v
 /- the axiom -/
 
 -- In the presence of classical logic, we could prove this from a weaker statement:
diff --git a/library/init/coe.lean b/library/init/coe.lean
index b0afde1b31..4d34dcb75a 100644
--- a/library/init/coe.lean
+++ b/library/init/coe.lean
@@ -25,7 +25,7 @@ a type to a sort.
 -/
 prelude
 import init.data.list.basic init.data.subtype.basic init.data.prod
-universe variables u v
+universes u v
 
 class has_lift (a : Sort u) (b : Sort v) :=
 (lift : a → b)
@@ -81,7 +81,7 @@ notation `⇑`:max x:max := coe_fn x
 
 notation `↥`:max x:max := coe_sort x
 
-universe variables u₁ u₂ u₃
+universes u₁ u₂ u₃
 
 /- Transitive closure for has_lift, has_coe, has_coe_to_fun -/
 
@@ -154,7 +154,7 @@ instance coe_subtype {a : Type u} {p : a → Prop} : has_coe {x // p x} a :=
 
 /- basic lifts -/
 
-universe variables ua ua₁ ua₂ ub ub₁ ub₂
+universes ua ua₁ ua₂ ub ub₁ ub₂
 
 /- Remark: we cant use [has_lift_t a₂ a₁] since it will produce non-termination whenever a type class resolution
    problem does not have a solution. -/
diff --git a/library/init/core.lean b/library/init/core.lean
index 3779225275..94e7d9064e 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -77,7 +77,7 @@ reserve infixl ` ++ `:65
 reserve infixr ` :: `:67
 reserve infixl `; `:1
 
-universe variables u v
+universes u v
 
 /-- Gadget for optional parameter support. -/
 @[reducible] def opt_param (α : Sort u) (default : α) : Sort u :=
@@ -603,7 +603,7 @@ lemma nat_add_zero (n : nat) : n + 0 = n := rfl
 
 /- Combinator calculus -/
 namespace combinator
-universe variables u₁ u₂ u₃
+universes u₁ u₂ u₃
 def I {α : Type u₁} (a : α) := a
 def K {α : Type u₁} {β : Type u₂} (a : α) (b : β) := a
 def S {α : Type u₁} {β : Type u₂} {γ : Type u₃} (x : α → β → γ) (y : α → β) (z : α) := x z (y z)
diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean
index a099c4e8fb..b19823cf98 100644
--- a/library/init/data/list/basic.lean
+++ b/library/init/data/list/basic.lean
@@ -10,7 +10,7 @@ open decidable list
 notation h :: t  := cons h t
 notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l
 
-universe variables u v w
+universes u v w
 
 instance (α : Type u) : inhabited (list α) :=
 ⟨list.nil⟩
diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean
index 9f292c6171..cf4dc52509 100644
--- a/library/init/data/list/instances.lean
+++ b/library/init/data/list/instances.lean
@@ -8,7 +8,7 @@ import init.category.monad init.category.alternative init.data.list.basic
 import init.meta.mk_dec_eq_instance
 open list
 
-universe variables u v
+universes u v
 
 @[inline] def list.bind {α : Type u} {β : Type v} (a : list α) (b : α → list β) : list β :=
 join (map b a)
diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean
index f07d4a9c43..1bf8811a2a 100644
--- a/library/init/data/list/lemmas.lean
+++ b/library/init/data/list/lemmas.lean
@@ -6,7 +6,7 @@ Author: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn
 prelude
 import init.data.list.basic init.function init.meta
 
-universe variables u v
+universes u v
 variables {α : Type u} {β : Type v}
 
 namespace list
diff --git a/library/init/data/option/basic.lean b/library/init/data/option/basic.lean
index 54db24c5eb..83aefb7493 100644
--- a/library/init/data/option/basic.lean
+++ b/library/init/data/option/basic.lean
@@ -7,7 +7,7 @@ prelude
 import init.logic init.category
 open decidable
 
-universe variables u v
+universes u v
 
 namespace option
 
diff --git a/library/init/data/prod.lean b/library/init/data/prod.lean
index b3deca10fe..4e86df46b6 100644
--- a/library/init/data/prod.lean
+++ b/library/init/data/prod.lean
@@ -5,7 +5,7 @@ Author: Leonardo de Moura, Jeremy Avigad
 -/
 prelude
 import init.logic
-universe variables u v
+universes u v
 
 instance {α : Type u} {β : Type v} [inhabited α] [inhabited β] : inhabited (prod α β) :=
 ⟨(default α, default β)⟩
diff --git a/library/init/data/quot.lean b/library/init/data/quot.lean
index 3c69076391..55e0da8547 100644
--- a/library/init/data/quot.lean
+++ b/library/init/data/quot.lean
@@ -9,7 +9,7 @@ prelude
 /- We import propext here, otherwise we would need a quot.lift for propositions. -/
 import init.data.sigma.basic init.logic init.propext init.data.setoid
 
-universe variables u v
+universes u v
 
 -- iff can now be used to do substitutions in a calculation
 attribute [subst]
@@ -144,7 +144,7 @@ quot.hrec_on q f c
 end
 
 section
-universe variables u_a u_b u_c
+universes u_a u_b u_c
 variables {α : Type u_a} {β : Type u_b} {φ : Type u_c}
 variables [s₁ : setoid α] [s₂ : setoid β]
 include s₁ s₂
@@ -214,7 +214,7 @@ end exact
 
 
 section
-universe variables u_a u_b u_c
+universes u_a u_b u_c
 variables {α : Type u_a} {β : Type u_b}
 variables [s₁ : setoid α] [s₂ : setoid β]
 include s₁ s₂
diff --git a/library/init/data/set.lean b/library/init/data/set.lean
index f10af71c1d..ad968cdd77 100644
--- a/library/init/data/set.lean
+++ b/library/init/data/set.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import init.logic init.category.functor
 
-universe variables u v
+universes u v
 def set (α : Type u) := α → Prop
 
 def set_of {α : Type u} (p : α → Prop) : set α :=
diff --git a/library/init/data/setoid.lean b/library/init/data/setoid.lean
index 2d537e1f42..166da36ff7 100644
--- a/library/init/data/setoid.lean
+++ b/library/init/data/setoid.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.logic
-universe variables u
+universes u
 class setoid (α : Type u) :=
 (r : α → α → Prop) (iseqv : equivalence r)
 
diff --git a/library/init/data/sigma/basic.lean b/library/init/data/sigma/basic.lean
index 25b13475ca..c97d54af2d 100644
--- a/library/init/data/sigma/basic.lean
+++ b/library/init/data/sigma/basic.lean
@@ -9,7 +9,7 @@ import init.logic init.wf
 notation `Σ` binders `, ` r:(scoped p, sigma p) := r
 notation `Σ'` binders `, ` r:(scoped p, psigma p) := r
 
-universe variables u v
+universes u v
 
 lemma ex_of_psig {α : Type u} {p : α → Prop} : (Σ' x, p x) → ∃ x, p x
 | ⟨x, hx⟩ := ⟨x, hx⟩
diff --git a/library/init/data/sigma/lex.lean b/library/init/data/sigma/lex.lean
index e18404ebb1..edf95f56ed 100644
--- a/library/init/data/sigma/lex.lean
+++ b/library/init/data/sigma/lex.lean
@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.data.sigma.basic init.meta
-universe variables u v
+universes u v
 namespace sigma
 section
   variables {α : Type u} {β : α → Type v}
diff --git a/library/init/data/subtype/basic.lean b/library/init/data/subtype/basic.lean
index fe2e121d07..8fdf0e255d 100644
--- a/library/init/data/subtype/basic.lean
+++ b/library/init/data/subtype/basic.lean
@@ -7,7 +7,7 @@ prelude
 import init.logic
 open decidable
 
-universe variables u
+universes u
 
 namespace subtype
 
diff --git a/library/init/data/subtype/instances.lean b/library/init/data/subtype/instances.lean
index 641f94f939..c3f8eec17f 100644
--- a/library/init/data/subtype/instances.lean
+++ b/library/init/data/subtype/instances.lean
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 prelude
 import init.meta.mk_dec_eq_instance init.data.subtype.basic
 open tactic subtype
-universe variables u
+universes u
 
 instance {α : Type u} {p : α → Prop} [decidable_eq α] : decidable_eq {x : α // p x} :=
 by mk_dec_eq_instance
diff --git a/library/init/data/sum/basic.lean b/library/init/data/sum/basic.lean
index b21185edba..f4f14c3790 100644
--- a/library/init/data/sum/basic.lean
+++ b/library/init/data/sum/basic.lean
@@ -10,7 +10,7 @@ import init.logic
 
 notation α ⊕ β := sum α β
 
-universe variables u v
+universes u v
 
 variables {α : Type u} {β : Type v}
 
diff --git a/library/init/data/sum/instances.lean b/library/init/data/sum/instances.lean
index 51549faab5..c0c40438ab 100644
--- a/library/init/data/sum/instances.lean
+++ b/library/init/data/sum/instances.lean
@@ -6,6 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import init.meta.mk_dec_eq_instance
 
-universe variables u v
+universes u v
 instance {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] : decidable_eq (α ⊕ β) :=
 by tactic.mk_dec_eq_instance
diff --git a/library/init/data/to_string.lean b/library/init/data/to_string.lean
index dac98ebbb4..98cff7368b 100644
--- a/library/init/data/to_string.lean
+++ b/library/init/data/to_string.lean
@@ -8,7 +8,7 @@ import init.data.string.basic init.data.bool.basic init.data.subtype.basic
 import init.data.unsigned init.data.prod init.data.sum.basic init.data.nat.div
 open sum subtype nat
 
-universe variables u v
+universes u v
 
 class has_to_string (α : Type u) :=
 (to_string : α → string)
diff --git a/library/init/function.lean b/library/init/function.lean
index 3e308852fe..3ebe8d458c 100644
--- a/library/init/function.lean
+++ b/library/init/function.lean
@@ -7,7 +7,7 @@ General operations on functions.
 -/
 prelude
 import init.data.prod init.funext init.logic
-universe variables u₁ u₂ u₃ u₄
+universes u₁ u₂ u₃ u₄
 
 namespace function
 notation f ` $ `:1 a:0 := f a
diff --git a/library/init/funext.lean b/library/init/funext.lean
index a83cf2f5fc..ef756d2ff0 100644
--- a/library/init/funext.lean
+++ b/library/init/funext.lean
@@ -8,7 +8,7 @@ Extensional equality for functions, and a proof of function extensionality from
 prelude
 import init.data.quot init.logic
 
-universe variables u v
+universes u v
 
 namespace function
 variables {α : Type u} {β : α → Type v}
diff --git a/library/init/logic.lean b/library/init/logic.lean
index efc26b4c92..b8066cad71 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 prelude
 import init.core
 
-universe variables u v w
+universes u v w
 
 @[reducible] def id {α : Sort u} (a : α) : α := a
 
diff --git a/library/init/meta/format.lean b/library/init/meta/format.lean
index a55e7cc091..bf0527dd09 100644
--- a/library/init/meta/format.lean
+++ b/library/init/meta/format.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import init.meta.options
 
-universe variables u v
+universes u v
 
 inductive format.color
 | red | green | orange | blue | pink | cyan | grey
diff --git a/library/init/meta/options.lean b/library/init/meta/options.lean
index 10471a8787..ee8601d813 100644
--- a/library/init/meta/options.lean
+++ b/library/init/meta/options.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.meta.name
-universe variables u
+universe u
 meta constant options                   : Type
 meta constant options.size              : options → nat
 meta constant options.mk                : options
diff --git a/library/init/meta/pexpr.lean b/library/init/meta/pexpr.lean
index 589d52ee65..3f5bcb4385 100644
--- a/library/init/meta/pexpr.lean
+++ b/library/init/meta/pexpr.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.meta.expr
-universe variables u
+universe u
 
 /- Quoted expressions. They can be converted into expressions by using a tactic. -/
 meta constant pexpr : Type
diff --git a/library/init/meta/smt/smt_tactic.lean b/library/init/meta/smt/smt_tactic.lean
index 39e1b8c638..873a62ea32 100644
--- a/library/init/meta/smt/smt_tactic.lean
+++ b/library/init/meta/smt/smt_tactic.lean
@@ -8,7 +8,7 @@ import init.meta.simp_tactic
 import init.meta.smt.congruence_closure
 import init.meta.smt.ematch
 
-universe variables u
+universe u
 
 run_command mk_simp_attr `pre_smt
 run_command mk_hinst_lemma_attr_set `ematch [] [`ematch_lhs]
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index abf3c8936d..4eaa172d0f 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -10,7 +10,7 @@ import init.data.nat.div init.meta.exceptional init.meta.format init.meta.enviro
 import init.meta.pexpr init.data.to_string init.data.string.basic
 meta constant tactic_state : Type
 
-universe variables u v
+universes u v
 
 namespace tactic_state
 meta constant env         : tactic_state → environment
diff --git a/library/init/propext.lean b/library/init/propext.lean
index 3d251c0644..474eb40490 100644
--- a/library/init/propext.lean
+++ b/library/init/propext.lean
@@ -9,7 +9,7 @@ import init.logic
 constant propext {a b : Prop} : (a ↔ b) → a = b
 
 /- Additional congruence lemmas. -/
-universe variables u v
+universes u v
 
 lemma forall_congr_eq {a : Sort u} {p q : a → Prop} (h : ∀ x, p x = q x) : (∀ x, p x) = ∀ x, q x :=
 propext (forall_congr (λ a, (h a)^.to_iff))
diff --git a/library/init/util.lean b/library/init/util.lean
index 20902ffe74..46dd492b0b 100644
--- a/library/init/util.lean
+++ b/library/init/util.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.data.string.basic
-universe variables u
+universes u
 
 /- This function has a native implementation that tracks time. -/
 def timeit {α : Type u} (s : string) (f : thunk α) : α :=
diff --git a/library/init/wf.lean b/library/init/wf.lean
index 91d1e4f900..1e6bbcf240 100644
--- a/library/init/wf.lean
+++ b/library/init/wf.lean
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 prelude
 import init.data.nat.basic init.data.prod
 
-universe variables u v
+universes u v
 
 inductive acc {α : Type u} (r : α → α → Prop) : α → Prop
 | intro : ∀ x, (∀ y, r y x → acc y) → acc x
diff --git a/library/tools/super/clausifier.lean b/library/tools/super/clausifier.lean
index 58966dfb3e..edcd2e6f40 100644
--- a/library/tools/super/clausifier.lean
+++ b/library/tools/super/clausifier.lean
@@ -7,7 +7,7 @@ import .clause .clause_ops
 import .prover_state .misc_preprocessing
 open expr list tactic monad decidable
 
-universe variable u
+universe u
 
 namespace super
 
diff --git a/src/api/lean_univ.h b/src/api/lean_univ.h
index ede9d78622..90e7152267 100644
--- a/src/api/lean_univ.h
+++ b/src/api/lean_univ.h
@@ -29,7 +29,6 @@ typedef enum {
     LEAN_UNIV_MAX,
     LEAN_UNIV_IMAX,
     LEAN_UNIV_PARAM,
-    LEAN_UNIV_GLOBAL,
     LEAN_UNIV_META
 } lean_univ_kind;
 
@@ -43,8 +42,6 @@ lean_bool lean_univ_mk_max(lean_univ u1, lean_univ u2, lean_univ * r, lean_excep
 lean_bool lean_univ_mk_imax(lean_univ u1, lean_univ u2, lean_univ * r, lean_exception * ex);
 /** \brief Create a universe parameter with the given name. */
 lean_bool lean_univ_mk_param(lean_name n, lean_univ * r, lean_exception * ex);
-/** \brief Create a reference to a global universe with the given name. */
-lean_bool lean_univ_mk_global(lean_name n, lean_univ * r, lean_exception * ex);
 /** \brief Create a universe meta-variable with the given name. */
 lean_bool lean_univ_mk_meta(lean_name n, lean_univ * r, lean_exception * ex);
 
@@ -70,7 +67,7 @@ lean_bool lean_univ_lt(lean_univ u1, lean_univ u2, lean_bool * b, lean_exception
     the hashcodes associated with \c u1 and \c u2. */
 lean_bool lean_univ_quick_lt(lean_univ u1, lean_univ u2, lean_bool * b, lean_exception * ex);
 /** \brief If \c r contains \c lean_true, then forall assignments \c A that assigns all parameters,
-    globals and metavariables occuring in \c u1 and \c u2, we have that the
+    and metavariables occuring in \c u1 and \c u2, we have that the
     universe level u1[A] is bigger or equal to u2[A]. */
 lean_bool lean_univ_geq(lean_univ u1, lean_univ u2, lean_bool * r, lean_exception * ex);
 
@@ -88,7 +85,6 @@ lean_bool lean_univ_get_max_lhs(lean_univ u, lean_univ * r, lean_exception * ex)
 lean_bool lean_univ_get_max_rhs(lean_univ u, lean_univ * r, lean_exception * ex);
 /** \brief Store the name of the given universe in \c r.
     \pre lean_univ_get_kind(u) == LEAN_UNIV_PARAM ||
-         lean_univ_get_kind(u) == LEAN_UNIV_GLOBAL ||
          lean_univ_get_kind(u) == LEAN_UNIV_META
     \remark exceptions: LEAN_OTHER_EXCEPTION */
 lean_bool lean_univ_get_name(lean_univ u, lean_name * r, lean_exception * ex);
diff --git a/src/api/univ.cpp b/src/api/univ.cpp
index d353e0d7eb..d951cd80b6 100644
--- a/src/api/univ.cpp
+++ b/src/api/univ.cpp
@@ -57,13 +57,6 @@ lean_bool lean_univ_mk_param(lean_name n, lean_univ * r, lean_exception * ex) {
     LEAN_CATCH;
 }
 
-lean_bool lean_univ_mk_global(lean_name n, lean_univ * r, lean_exception * ex) {
-    LEAN_TRY;
-    check_nonnull(n);
-    *r = of_level(new level(mk_global_univ(to_name_ref(n))));
-    LEAN_CATCH;
-}
-
 lean_bool lean_univ_mk_meta(lean_name n, lean_univ * r, lean_exception * ex) {
     LEAN_TRY;
     check_nonnull(n);
@@ -103,8 +96,8 @@ lean_univ_kind lean_univ_get_kind(lean_univ u) {
     case level_kind::Max:      return LEAN_UNIV_MAX;
     case level_kind::IMax:     return LEAN_UNIV_IMAX;
     case level_kind::Param:    return LEAN_UNIV_PARAM;
-    case level_kind::Global:   return LEAN_UNIV_GLOBAL;
     case level_kind::Meta:     return LEAN_UNIV_META;
+    case level_kind::Global:   break; // TODO(Leo): delete
     }
     lean_unreachable();
 }
@@ -179,8 +172,6 @@ lean_bool lean_univ_get_name(lean_univ u, lean_name * r, lean_exception * ex) {
     check_nonnull(u);
     if (lean_univ_get_kind(u) == LEAN_UNIV_PARAM)
         *r = of_name(new name(param_id(to_level_ref(u))));
-    else if (lean_univ_get_kind(u) == LEAN_UNIV_GLOBAL)
-        *r = of_name(new name(global_id(to_level_ref(u))));
     else if (lean_univ_get_kind(u) == LEAN_UNIV_META)
         *r = of_name(new name(meta_id(to_level_ref(u))));
     else
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 9ec18935f1..25b447defe 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -30,6 +30,7 @@ Author: Leonardo de Moura
 #include "library/reducible.h"
 #include "library/typed_expr.h"
 #include "library/documentation.h"
+#include "library/placeholder.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_string.h"
 #include "library/compiler/vm_compiler.h"
@@ -134,7 +135,7 @@ static environment redeclare_aliases(environment env, parser & p,
     name_set popped_levels;
     local_level_decls level_decls = p.get_local_level_decls();
     old_level_decls.for_each([&](name const & n, level const & l) {
-            if (is_param(l) && !level_decls.contains(n))
+            if (is_param(l) && !is_placeholder(l) && !level_decls.contains(n))
                 popped_levels.insert(param_id(l));
         });
     for (auto const & entry : to_redeclare) {
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index a33a5aaebb..1fd2159378 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -43,11 +43,7 @@ static environment declare_universe(parser & p, environment env, name const & n,
     } else if (in_section(env)) {
         p.add_local_level(n, mk_param_univ(n), false);
     } else {
-        name const & ns = get_namespace(env);
-        name full_n  = ns + n;
-        env = module::add_universe(env, full_n);
-        if (!ns.is_anonymous())
-            env = add_level_alias(env, n, full_n);
+        p.add_local_level(n, mk_param_univ(n), true);
     }
     return env;
 }
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 96b4659b31..f9a8b3a85e 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -3062,7 +3062,7 @@ struct sanitize_param_names_fn : public replace_visitor {
     level sanitize(level const & l) {
         name p("u");
         return replace(l, [&](level const & l) -> optional<level> {
-                if (is_param(l)) {
+                if (is_param(l) && !is_placeholder(l)) {
                     name const & n = param_id(l);
                     if (is_tagged_by(n, *g_level_prefix)) {
                         if (auto new_l = m_R.find(n)) {
diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp
index 9e9285a618..f5b4e57a94 100644
--- a/src/frontends/lean/inductive_cmds.cpp
+++ b/src/frontends/lean/inductive_cmds.cpp
@@ -489,8 +489,7 @@ public:
     inductive_cmd_fn(parser & p, decl_attributes const & attrs, bool is_trusted):
         m_p(p), m_env(p.env()), m_attrs(attrs),
         m_is_trusted(is_trusted), m_ctx(p.env()) {
-        m_env = m_env.add_universe(tmp_global_univ_name());
-        m_u = mk_global_univ(tmp_global_univ_name());
+        m_u = mk_param_univ(tmp_global_univ_name());
         check_attrs(m_attrs);
         m_doc_string = p.get_doc_string();
     }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index c19230b241..c0eca28aa4 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -740,16 +740,6 @@ level parser::parse_level_id() {
     if (auto it = m_local_level_decls.find(id))
         return *it;
 
-    for (name const & ns : get_namespaces(m_env)) {
-        auto new_id = ns + id;
-        if (!ns.is_anonymous() && m_env.is_universe(new_id))
-            return mk_global_univ(new_id);
-    }
-
-    if (m_env.is_universe(id))
-        return mk_global_univ(id);
-    if (auto it = get_level_alias(m_env, id))
-        return mk_global_univ(*it);
     throw parser_error(sstream() << "unknown universe '" << id << "'", p);
 }
 
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index a6889f3a52..2212931ef9 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -119,7 +119,7 @@ void remove_local_vars(parser const & p, buffer<expr> & locals) {
 
 levels remove_local_vars(parser const & p, levels const & ls) {
     return filter(ls, [&](level const & l) {
-            return !is_param(l) || !p.is_local_level_variable(param_id(l));
+            return is_placeholder(l) || !is_param(l) || !p.is_local_level_variable(param_id(l));
         });
 }
 
diff --git a/src/library/aux_definition.cpp b/src/library/aux_definition.cpp
index 6a744df6f6..6110b545e7 100644
--- a/src/library/aux_definition.cpp
+++ b/src/library/aux_definition.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/replace_fn.h"
 #include "library/locals.h"
+#include "library/placeholder.h"
 #include "library/module.h"
 #include "library/trace.h"
 #include "library/aux_definition.h"
@@ -47,6 +48,7 @@ struct mk_aux_definition_fn {
                         return some_level(new_r);
                     }
                 } else if (is_param(l)) {
+                    lean_assert(!is_placeholder(l));
                     name const & id = param_id(l);
                     if (!m_found_univ_params.contains(id)) {
                         m_found_univ_params.insert(id);
diff --git a/src/library/locals.cpp b/src/library/locals.cpp
index 948c7611d9..d2960aef08 100644
--- a/src/library/locals.cpp
+++ b/src/library/locals.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/find_fn.h"
+#include "library/placeholder.h"
 #include "library/locals.h"
 
 namespace lean {
@@ -17,7 +18,7 @@ void collect_univ_params_core(level const & l, name_set & r) {
     for_each(l, [&](level const & l) {
             if (!has_param(l))
                 return false;
-            if (is_param(l))
+            if (is_param(l) && !is_placeholder(l))
                 r.insert(param_id(l));
             return true;
         });
diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp
index 5be3acf409..aab666ec22 100644
--- a/src/library/placeholder.cpp
+++ b/src/library/placeholder.cpp
@@ -36,8 +36,8 @@ static unsigned next_placeholder_id() {
     g_placeholder_id++;
     return r;
 }
-level mk_level_placeholder() { return mk_global_univ(name(*g_placeholder_name, next_placeholder_id())); }
-level mk_level_one_placeholder() { return mk_global_univ(*g_placeholder_one_name); }
+level mk_level_placeholder() { return mk_param_univ(name(*g_placeholder_name, next_placeholder_id())); }
+level mk_level_one_placeholder() { return mk_param_univ(*g_placeholder_one_name); }
 static name const & to_prefix(expr_placeholder_kind k) {
     switch (k) {
     case expr_placeholder_kind::Implicit:       return *g_implicit_placeholder_name;
@@ -65,8 +65,8 @@ static bool is_strict_placeholder(name const & n) {
 static bool is_explicit_placeholder(name const & n) {
     return !n.is_atomic() && n.get_prefix() == *g_explicit_placeholder_name;
 }
-bool is_placeholder(level const & e) { return is_global(e) && is_placeholder(global_id(e)); }
-bool is_one_placeholder(level const & e) { return is_global(e) && global_id(e) == *g_placeholder_one_name; }
+bool is_placeholder(level const & e) { return is_param(e) && is_placeholder(param_id(e)); }
+bool is_one_placeholder(level const & e) { return is_param(e) && param_id(e) == *g_placeholder_one_name; }
 
 bool is_placeholder(expr const & e) {
     return (is_constant(e) && is_placeholder(const_name(e))) || (is_local(e) && is_placeholder(mlocal_name(e)));
diff --git a/src/tests/shared/univ.c b/src/tests/shared/univ.c
index 23bb4a307d..d6e0a1adef 100644
--- a/src/tests/shared/univ.c
+++ b/src/tests/shared/univ.c
@@ -19,7 +19,7 @@ void check_core(int v, unsigned l) {
 
 int main() {
     lean_exception ex;
-    lean_name a, l, U, pp, pp_unicode, rn;
+    lean_name a, l, pp, pp_unicode, rn;
     lean_options o1, o2;
     lean_univ zero, one, p1, g1, m1, u, n, i, ru;
     lean_list_name ln1, ln2;
@@ -29,7 +29,6 @@ int main() {
 
     check(lean_name_mk_anonymous(&a, &ex));
     check(lean_name_mk_str(a, "l_1", &l, &ex));
-    check(lean_name_mk_str(a, "U", &U, &ex));
     check(lean_name_mk_str(a, "pp", &pp, &ex));
     check(lean_name_mk_str(pp, "unicode", &pp_unicode, &ex));
 
@@ -39,7 +38,6 @@ int main() {
     check(lean_univ_mk_zero(&zero, &ex));
     check(lean_univ_mk_succ(zero, &one, &ex));
     check(lean_univ_mk_param(l, &p1, &ex));
-    check(lean_univ_mk_global(U, &g1, &ex));
     check(lean_univ_mk_max(p1, one, &m1, &ex));
     check(lean_univ_mk_succ(m1, &u, &ex));
 
@@ -67,7 +65,6 @@ int main() {
     check(lean_univ_get_kind(one) == LEAN_UNIV_SUCC);
     check(lean_univ_get_kind(n) == LEAN_UNIV_MAX);
 
-    check(lean_univ_get_name(g1, &rn, &ex) && lean_name_eq(rn, U));
 
     check(lean_univ_get_max_lhs(m1, &ru, &ex) && lean_univ_eq(ru, p1, &r, &ex) && r);
     lean_univ_del(ru);
@@ -78,7 +75,6 @@ int main() {
 
     lean_name_del(a);
     lean_name_del(l);
-    lean_name_del(U);
     lean_name_del(pp);
     lean_name_del(pp_unicode);
     lean_name_del(rn);
diff --git a/tests/lean/run/cc5.lean b/tests/lean/run/cc5.lean
index 6c661f01ac..23093bc876 100644
--- a/tests/lean/run/cc5.lean
+++ b/tests/lean/run/cc5.lean
@@ -1,8 +1,7 @@
-universes l1 l2 l3 l4 l5 l6
-constants (A : Type l1) (B : A → Type l2) (C : ∀ (a : A) (ba : B a), Type l3)
-          (D : ∀ (a : A) (ba : B a) (cba : C a ba), Type l4)
-          (E : ∀ (a : A) (ba : B a) (cba : C a ba) (dcba : D a ba cba), Type l5)
-          (F : ∀ (a : A) (ba : B a) (cba : C a ba) (dcba : D a ba cba) (edcba : E a ba cba dcba), Type l6)
+constants (A : Type) (B : A → Type) (C : ∀ (a : A) (ba : B a), Type)
+          (D : ∀ (a : A) (ba : B a) (cba : C a ba), Type)
+          (E : ∀ (a : A) (ba : B a) (cba : C a ba) (dcba : D a ba cba), Type)
+          (F : ∀ (a : A) (ba : B a) (cba : C a ba) (dcba : D a ba cba) (edcba : E a ba cba dcba), Type)
           (C_ss : ∀ a ba, subsingleton (C a ba))
           (a1 a2 a3 : A)
           (mk_B1 mk_B2 : ∀ a, B a)
diff --git a/tests/lean/run/lift2.lean b/tests/lean/run/lift2.lean
index 4c791dbef3..c045e507e9 100644
--- a/tests/lean/run/lift2.lean
+++ b/tests/lean/run/lift2.lean
@@ -7,7 +7,7 @@ set_option pp.universes true
 variables (A : Type 3) (B : Type 1)
 check A = lift.{1 3} B
 
-universe u
+universe variables u
 variables (C : Type (u+2)) (D : Type u)
 check C = lift.{u u+2} D
 end test
diff --git a/tests/lean/run/simplifier_custom_relations.lean b/tests/lean/run/simplifier_custom_relations.lean
index c1d3cf23db..0590d0234d 100644
--- a/tests/lean/run/simplifier_custom_relations.lean
+++ b/tests/lean/run/simplifier_custom_relations.lean
@@ -1,7 +1,7 @@
 open tactic
 
-universe l
-constants (A : Type.{l}) (rel : A → A → Prop)
+
+constants (A : Type) (rel : A → A → Prop)
           (rel.refl : ∀ a, rel a a)
           (rel.symm : ∀ a b, rel a b → rel b a)
           (rel.trans : ∀ a b c, rel a b → rel b c → rel a c)
diff --git a/tests/lean/run/t2.lean b/tests/lean/run/t2.lean
index b5f2b34745..9cc3da13a5 100644
--- a/tests/lean/run/t2.lean
+++ b/tests/lean/run/t2.lean
@@ -1,5 +1,5 @@
-universe l
-universe u
+universe variable l
+universe variable u
 print raw Type
 print raw Type.{1}
 print raw Type.{2}
diff --git a/tests/lean/run/univ1.lean b/tests/lean/run/univ1.lean
index 8946c0974b..49b9d3bf6d 100644
--- a/tests/lean/run/univ1.lean
+++ b/tests/lean/run/univ1.lean
@@ -7,7 +7,7 @@ axiom iso1 : ∀x, foldd (unfoldd x) = x
 end S1
 
 namespace S2
-universe u
+universe variables u
 axiom I : Type.{u}
 definition F (X : Type*) : Type* := (X → Prop) → Prop
 axiom unfoldd : I → F I
diff --git a/tests/lean/t3.lean b/tests/lean/t3.lean
deleted file mode 100644
index f87c2d8b16..0000000000
--- a/tests/lean/t3.lean
+++ /dev/null
@@ -1,35 +0,0 @@
-universe u
-print raw Type.{u}
-namespace tst
-  universe v
-  print raw Type.{v}
-  print raw Type.{tst.v}
-end tst
-print raw Type.{tst.v}
-print raw Type.{v}  -- Error: alias 'v' is not available anymore
-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
-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
-  print raw Type.{u}
-  namespace foo
-    universe U
-  end foo
-end tst
-print raw Type.{tst.foo.U}
-namespace tst
-  namespace foo
-    print raw Type.{v}  -- Remark: alias 'v' for 'tst.v' is available again
-    print raw Type.{U}  -- Remark: alias 'U' for 'tst.foo.U' is available again
-  end foo
-end tst
-namespace bla
-  universe u -- Error: we cannot shadow universe levels
-end bla
-print raw Type.{bla.u} -- Error: we failed to declare bla.u
diff --git a/tests/lean/t3.lean.expected.out b/tests/lean/t3.lean.expected.out
deleted file mode 100644
index 8b50feb54d..0000000000
--- a/tests/lean/t3.lean.expected.out
+++ /dev/null
@@ -1,15 +0,0 @@
-Type u
-Type tst.v
-Type tst.v
-Type tst.v
-t3.lean:9:16: error: unknown universe 'v'
-Type z
-t3.lean:14:16: error: unknown universe 'z'
-t3.lean:16:2: error: invalid namespace declaration, a namespace cannot be declared inside a section
-Type tst.v
-Type u
-Type tst.foo.U
-Type tst.v
-Type tst.foo.U
-t3.lean:33:2: error: universe level alias 'u' shadows existing global universe level
-t3.lean:35:16: error: unknown universe 'bla.u'
diff --git a/tests/lean/univ_vars.lean b/tests/lean/univ_vars.lean
index 92f4c7848d..ceb61b9c7f 100644
--- a/tests/lean/univ_vars.lean
+++ b/tests/lean/univ_vars.lean
@@ -1,7 +1,7 @@
 --
 set_option pp.universes true
 
-universe u
+universe variable u
 variable A : Type.{u}
 
 definition id1 (a : A) : A := a
diff --git a/tests/lean/univ_vars.lean.expected.out b/tests/lean/univ_vars.lean.expected.out
index e614f6a58a..35e5098cc2 100644
--- a/tests/lean/univ_vars.lean.expected.out
+++ b/tests/lean/univ_vars.lean.expected.out
@@ -1,4 +1,4 @@
-id1 : Π (A : Type u), A → A
+id1.{u_1} : Π (A : Type u_1), A → A
 id2 : Π (B : Type), B → B
 id3.{u_1} : Π (C : Type u_1), C → C
 foo.{u_1} : Π (A₁ A₂ : Type u_1), A₁ → A₂ → Prop