feat(frontends/lean): no global universes in the frontend

2017-02-08 17:19:49 -08:00 · 2017-02-08 17:19:49 -08:00 · 32e6442d0a
commit 32e6442d0a
parent c5dc8e651a
74 changed files with 87 additions and 167 deletions
--- 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
--- 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

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

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

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

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

--- 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 α,
--- 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 α :=
--- 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))
--- 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)
--- 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)
--- 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 β)
--- 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)
--- 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)
--- 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)
--- 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)
--- 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:
--- 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. -/
--- 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)
--- 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⟩
--- 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)
--- 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
--- 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

--- 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 β)⟩
--- 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₂
--- 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 α :=
--- 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)

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

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

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

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

--- 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);
--- 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
--- 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) {
--- 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;
 }
--- 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)) {
--- 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();
    }
--- 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);
 }

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

--- 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);
--- 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;
        });
--- 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)));
--- 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);
--- 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)
--- 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
--- 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)
--- 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}
--- 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
--- a/tests/lean/t3.lean
+++ b/tests/lean/t3.lean
@ -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
--- a/tests/lean/t3.lean.expected.out
+++ b/tests/lean/t3.lean.expected.out
@ -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'
--- 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
--- 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