diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 1c24edd68..72ccbd2e1 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -1,7 +1,7 @@
 import macros
 
-universe M : 512
-universe U : M+512
+universe M ≥ 512
+universe U ≥ M+512
 
 variable Bool : Type
 -- The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions
diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp
index fa6ee1ebe..19e906703 100644
--- a/src/frontends/lean/parser_cmds.cpp
+++ b/src/frontends/lean/parser_cmds.cpp
@@ -619,7 +619,7 @@ void parser_imp::parse_help() {
                             << "  set::opaque [id] [bool]  set the given definition as opaque/transparent" << endl
                             << "  theorem [id] : [type] := [expr]    define a new theorem" << endl
                             << "  variable [id] : [type]   declare/postulate an element of the given type" << endl
-                            << "  universe [id] [level]    declare a new universe variable that is >= the given level" << endl
+                            << "  universe [id] >= [level] declare a new universe constraint" << endl
                             << "  using [id]_1 [id]_2?     create an alias for object starting with the prefix [id]_1 using the [id]_2" << endl;
 #if !defined(LEAN_WINDOWS)
         regular(m_io_state) << "Type Ctrl-D to exit" << endl;
@@ -650,12 +650,17 @@ void parser_imp::parse_cmd_macro(name cmd_id, pos_info const & p) {
     parse_macro(m.m_arg_kinds, m.m_fn, m.m_precedence, args, p);
 }
 
+static name g_geq_unicode("\u2265"); // ≥
+static name g_geq(">=");
+
 void parser_imp::parse_universe() {
     next();
-    name id   = check_identifier_next("invalid universe declaration, identifier expected");
-    check_colon_next("invalid universe declaration, ':' expected");
+    name id   = check_identifier_next("invalid universe constraint, identifier expected");
+    name geq  = check_identifier_next("invalid universe constraint, '>=' expected");
+    if (geq != g_geq && geq != g_geq_unicode)
+        throw parser_error("invalid universe constraint, '>=' expected", m_last_cmd_pos);
     level lvl = parse_level();
-    m_env->add_uvar(id, lvl);
+    m_env->add_uvar_cnstr(id, lvl);
 }
 
 void parser_imp::parse_alias() {
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index c9f6bf963..4ead0ef7c 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1318,7 +1318,7 @@ class pp_formatter_cell : public formatter_cell {
         }
     }
 
-    format pp_uvar_decl(object const & obj, options const & opts) {
+    format pp_uvar_cnstr(object const & obj, options const & opts) {
         bool unicode = get_pp_unicode(opts);
         return format{highlight_command(format(obj.keyword())), space(), format(obj.get_name()), space(), format(unicode ? "\u2265" : ">="), space(), ::lean::pp(obj.get_cnstr_level(), unicode)};
     }
@@ -1412,7 +1412,7 @@ public:
 
     virtual format operator()(object const & obj, options const & opts) {
         switch (obj.kind()) {
-        case object_kind::UVarDeclaration:  return pp_uvar_decl(obj, opts);
+        case object_kind::UVarConstraint:   return pp_uvar_cnstr(obj, opts);
         case object_kind::Postulate:        return pp_postulate(obj, opts);
         case object_kind::Definition:       return pp_definition(obj, opts);
         case object_kind::Builtin:          return pp_postulate(obj, opts);
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index a8b9f8c7d..8a6a7f8a5 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -24,6 +24,7 @@ Author: Leonardo de Moura
 #include "kernel/threadsafe_environment.h"
 #include "kernel/type_checker.h"
 #include "kernel/normalizer.h"
+#include "kernel/universe_constraints.h"
 #include "version.h"
 
 namespace lean {
@@ -232,17 +233,34 @@ object environment_cell::get_object(name const & n) const {
     }
 }
 
-/**
-   \brief Return true if u >= v + k is implied by constraints
-   \pre is_uvar(u) && is_uvar(v)
-*/
-bool environment_cell::is_implied(level const & u, level const & v, int k) const {
-    lean_assert(is_uvar(u) && is_uvar(v));
-    if (u == v)
-        return k <= 0;
-    else
-        return std::any_of(m_constraints.begin(), m_constraints.end(),
-                           [&](constraint const & c) { return std::get<0>(c) == u && std::get<1>(c) == v && std::get<2>(c) >= k; });
+struct universes {
+    std::vector<level>                  m_uvars;
+    universe_constraints                m_constraints;
+};
+
+universes & environment_cell::get_rw_universes() {
+    if (!m_universes) {
+        lean_assert(has_parent());
+        m_universes.reset(new universes(m_parent->get_rw_universes()));
+    }
+    return *m_universes;
+}
+
+universes const & environment_cell::get_ro_universes() const {
+    if (m_universes) {
+        return *m_universes;
+    } else {
+        lean_assert(has_parent());
+        return m_parent->get_ro_universes();
+    }
+}
+
+universe_constraints & environment_cell::get_rw_ucs() {
+    return get_rw_universes().m_constraints;
+}
+
+universe_constraints const & environment_cell::get_ro_ucs() const {
+    return get_ro_universes().m_constraints;
 }
 
 /** \brief Return true iff l1 >= l2 + k by asserted universe constraints. */
@@ -252,7 +270,7 @@ bool environment_cell::is_ge(level const & l1, level const & l2, int k) const {
     switch (kind(l2)) {
     case level_kind::UVar:
         switch (kind(l1)) {
-        case level_kind::UVar: return is_implied(l1, l2, k);
+        case level_kind::UVar: return get_ro_ucs().is_implied(uvar_name(l1), uvar_name(l2), k);
         case level_kind::Lift: return is_ge(lift_of(l1), l2, safe_sub(k, lift_offset(l1)));
         case level_kind::Max:  return std::any_of(max_begin_levels(l1), max_end_levels(l1), [&](level const & l) { return is_ge(l, l2, k); });
         }
@@ -264,70 +282,66 @@ bool environment_cell::is_ge(level const & l1, level const & l2, int k) const {
 
 /** \brief Return true iff l1 >= l2 is implied by asserted universe constraints. */
 bool environment_cell::is_ge(level const & l1, level const & l2) const {
-    if (has_parent())
-        return m_parent->is_ge(l1, l2);
-    else
-        return is_ge(l1, l2, 0);
+    return is_ge(l1, l2, 0);
 }
 
 /** \brief Add a new universe variable */
 level environment_cell::add_uvar_core(name const & n) {
     check_name(n);
+    universes & u = get_rw_universes();
+    u.m_constraints.add_var(n);
     level r(n);
-    m_uvars.push_back(r);
+    u.m_uvars.push_back(r);
     return r;
 }
 
-/**
-   \brief Add basic constraint u >= v + d, and all basic
-   constraints implied by transitivity.
-
-   \pre is_uvar(u) && is_uvar(v)
-*/
-void environment_cell::add_constraint(level const & u, level const & v, int d) {
-    lean_assert(is_uvar(u) && is_uvar(v));
-    if (is_implied(u, v, d))
-        return; // redundant
-    buffer<constraint> to_add;
-    for (constraint const & c : m_constraints) {
-        if (std::get<0>(c) == v) {
-            level const & l3 = std::get<1>(c);
-            int u_l3_d = safe_add(d, std::get<2>(c));
-            if (!is_implied(u, l3, u_l3_d))
-                to_add.emplace_back(u, l3, u_l3_d);
-        }
-    }
-    m_constraints.emplace_back(u, v, d);
-    for (constraint const & c : to_add) {
-        m_constraints.push_back(c);
-    }
-}
-
 /**
    \brief Add all basic constraints implied by n >= l + k
 
    A basic constraint is a constraint of the form u >= v + k
    where u and v are universe variables.
 */
-void environment_cell::add_constraints(level const & n, level const & l, int k) {
-    lean_assert(is_uvar(n));
+void environment_cell::add_constraints(name const & n, level const & l, int k) {
     switch (kind(l)) {
-    case level_kind::UVar: add_constraint(n, l, k); return;
+    case level_kind::UVar: get_rw_ucs().add_constraint(n, uvar_name(l), k); return;
     case level_kind::Lift: add_constraints(n, lift_of(l), safe_add(k, lift_offset(l))); return;
     case level_kind::Max:  std::for_each(max_begin_levels(l), max_end_levels(l), [&](level const & l1) { add_constraints(n, l1, k); }); return;
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
+/**
+   \brief Check if n >= l + k is consistent with the existing constraints.
+*/
+void environment_cell::check_consistency(name const & n, level const & l, int k) const {
+    switch (kind(l)) {
+    case level_kind::UVar:
+        if (!get_ro_ucs().is_consistent(n, uvar_name(l), k))
+            throw kernel_exception(env(), sstream() << "universe constraint inconsistency: " << n << " >= " << l << " + " << k);
+        return;
+    case level_kind::Lift: check_consistency(n, lift_of(l), safe_add(k, lift_offset(l))); return;
+    case level_kind::Max:  std::for_each(max_begin_levels(l), max_end_levels(l), [&](level const & l1) { check_consistency(n, l1, k); }); return;
+    }
+    lean_unreachable(); // LCOV_EXCL_LINE
+}
+
 /** \brief Add a new universe variable with constraint n >= l */
-level environment_cell::add_uvar(name const & n, level const & l) {
-    if (has_parent())
-        throw kernel_exception(env(), "invalid universe declaration, universe variables can only be declared in top-level environments");
+level environment_cell::add_uvar_cnstr(name const & n, level const & l) {
     if (has_children())
         throw read_only_environment_exception(env());
-    level r = add_uvar_core(n);
-    add_constraints(r, l, 0);
-    register_named_object(mk_uvar_decl(n, l));
+    level r;
+    auto const & uvs = get_ro_universes().m_uvars;
+    auto it = std::find_if(uvs.begin(), uvs.end(), [&](level const & l) { return uvar_name(l) == n; });
+    if (it == uvs.end()) {
+        r = add_uvar_core(n);
+        register_named_object(mk_uvar_cnstr(n, l));
+    } else {
+        // universe n already exists, we must check consistency of the new constraint.
+        check_consistency(n, l, 0);
+        r = *it;
+        m_objects.push_back(mk_uvar_cnstr(n, l));
+    }
+    add_constraints(n, l, 0);
     return r;
 }
 
@@ -337,22 +351,23 @@ level environment_cell::add_uvar(name const & n, level const & l) {
    contain a universe variable named \c n.
 */
 level environment_cell::get_uvar(name const & n) const {
-    if (has_parent()) {
-        return m_parent->get_uvar(n);
-    } else {
-        auto it = std::find_if(m_uvars.begin(), m_uvars.end(), [&](level const & l) { return uvar_name(l) == n; });
-        if (it == m_uvars.end())
-            throw unknown_universe_variable_exception(env(), n);
-        else
-            return *it;
-    }
+    auto const & uvs = get_ro_universes().m_uvars;
+    auto it = std::find_if(uvs.begin(), uvs.end(), [&](level const & l) { return uvar_name(l) == n; });
+    if (it == uvs.end())
+        throw unknown_universe_variable_exception(env(), n);
+    else
+        return *it;
 }
 
 /**
    \brief Initialize the set of universe variables with bottom
 */
 void environment_cell::init_uvars() {
-    m_uvars.emplace_back();
+    m_universes.reset(new universes());
+    universes & u = get_rw_universes();
+    level bottom;
+    u.m_uvars.push_back(bottom);
+    u.m_constraints.add_var(uvar_name(bottom));
 }
 
 /**
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index c0fd83817..3e7b72f89 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -23,6 +23,8 @@ class environment;
 class ro_environment;
 class type_checker;
 class environment_extension;
+class universe_constraints;
+class universes;
 
 /** \brief Implementation of the Lean environment. */
 class environment_cell {
@@ -34,8 +36,7 @@ class environment_cell {
     typedef std::tuple<level, level, int> constraint;
     std::weak_ptr<environment_cell>         m_this;
     // Universe variable management
-    std::vector<constraint>                 m_constraints;
-    std::vector<level>                      m_uvars;
+    std::unique_ptr<universes>              m_universes;
     // Children environment management
     atomic<unsigned>                        m_num_children;
     std::shared_ptr<environment_cell>       m_parent;
@@ -68,11 +69,15 @@ class environment_cell {
     void register_named_object(object const & new_obj);
     optional<object> get_object_core(name const & n) const;
 
-    bool is_implied(level const & u, level const & v, int k) const;
-    bool is_ge(level const & l1, level const & l2, int k) const;
+    universes & get_rw_universes();
+    universes const & get_ro_universes() const;
+    universe_constraints & get_rw_ucs();
+    universe_constraints const & get_ro_ucs() const;
+
     level add_uvar_core(name const & n);
-    void add_constraint(level const & u, level const & v, int d);
-    void add_constraints(level const & n, level const & l, int k);
+    bool is_ge(level const & l1, level const & l2, int k) const;
+    void check_consistency(name const & n, level const & l, int k) const;
+    void add_constraints(name const & n, level const & l, int k);
     void init_uvars();
     void check_no_cached_type(expr const & e);
     void check_type(name const & n, expr const & t, expr const & v);
@@ -107,13 +112,13 @@ public:
     // =======================================
     // Universe variables
     /**
-       \brief Add a new universe variable with name \c n and constraint <tt>n >= l</tt>.
-       Return the new variable.
+       \brief Add a new universe variable constraint of the form <tt>n >= l</tt>.
+       Return the level of \c n.
 
        \remark An exception is thrown if a universe inconsistency is detected.
     */
-    level add_uvar(name const & n, level const & l);
-    level add_uvar(name const & n) { return add_uvar(n, level()); }
+    level add_uvar_cnstr(name const & n, level const & l);
+    level add_uvar_cnstr(name const & n) { return add_uvar_cnstr(n, level()); }
 
     /**
        \brief Return true iff the constraint l1 >= l2 is implied by the constraints
diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp
index e701b79ab..9987b7788 100644
--- a/src/kernel/object.cpp
+++ b/src/kernel/object.cpp
@@ -47,26 +47,26 @@ public:
 };
 
 /**
-   \brief Universe variable name declaration.
+   \brief Universe variable constraint.
 */
-class uvar_declaration_object_cell : public named_object_cell {
+class uvar_constraint_object_cell : public named_object_cell {
     level m_level;
 public:
-    uvar_declaration_object_cell(name const & n, level const & l):
-        named_object_cell(object_kind::UVarDeclaration, n), m_level(l) {}
-    virtual ~uvar_declaration_object_cell() {}
+    uvar_constraint_object_cell(name const & n, level const & l):
+        named_object_cell(object_kind::UVarConstraint, n), m_level(l) {}
+    virtual ~uvar_constraint_object_cell() {}
 
     virtual bool has_cnstr_level() const  { return true; }
     virtual level get_cnstr_level() const { return m_level; }
     virtual char const * keyword() const  { return "universe"; }
     virtual void write(serializer & s) const { s << "universe" << get_name() << m_level; }
 };
-static void read_uvar_decl(environment const & env, io_state const &, deserializer & d) {
+static void read_uvar_cnstr(environment const & env, io_state const &, deserializer & d) {
     name n    = read_name(d);
     level lvl = read_level(d);
-    env->add_uvar(n, lvl);
+    env->add_uvar_cnstr(n, lvl);
 }
-static object_cell::register_deserializer_fn uvar_ds("universe", read_uvar_decl);
+static object_cell::register_deserializer_fn uvar_ds("universe", read_uvar_cnstr);
 
 /**
    \brief Builtin object.
@@ -233,7 +233,7 @@ static void read_theorem(environment const & env, io_state const &, deserializer
 }
 static object_cell::register_deserializer_fn theorem_ds("th", read_theorem);
 
-object mk_uvar_decl(name const & n, level const & l) { return object(new uvar_declaration_object_cell(n, l)); }
+object mk_uvar_cnstr(name const & n, level const & l) { return object(new uvar_constraint_object_cell(n, l)); }
 object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight) { return object(new definition_object_cell(n, t, v, weight)); }
 object mk_theorem(name const & n, expr const & t, expr const & v) { return object(new theorem_object_cell(n, t, v)); }
 object mk_axiom(name const & n, expr const & t) { return object(new axiom_object_cell(n, t)); }
diff --git a/src/kernel/object.h b/src/kernel/object.h
index 329e4c998..c33c8fca6 100644
--- a/src/kernel/object.h
+++ b/src/kernel/object.h
@@ -18,7 +18,7 @@ Author: Leonardo de Moura
 namespace lean {
 class io_state;
 class object;
-enum class object_kind { UVarDeclaration, Definition, Postulate, Builtin, BuiltinSet, Neutral };
+enum class object_kind { UVarConstraint, Definition, Postulate, Builtin, BuiltinSet, Neutral };
 
 class object_cell {
 protected:
@@ -111,7 +111,7 @@ public:
 
     object_kind kind() const { return m_ptr->kind(); }
 
-    friend object mk_uvar_decl(name const & n, level const & l);
+    friend object mk_uvar_cnstr(name const & n, level const & l);
     friend object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight);
     friend object mk_theorem(name const & n, expr const & t, expr const & v);
     friend object mk_axiom(name const & n, expr const & t);
@@ -148,7 +148,7 @@ inline optional<object> none_object() { return optional<object>(); }
 inline optional<object> some_object(object const & o) { return optional<object>(o); }
 inline optional<object> some_object(object && o) { return optional<object>(std::forward<object>(o)); }
 
-object mk_uvar_decl(name const & n, level const & l);
+object mk_uvar_cnstr(name const & n, level const & l);
 object mk_builtin(expr const & v);
 object mk_builtin_set(expr const & r);
 object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight);
diff --git a/src/kernel/universe_constraints.cpp b/src/kernel/universe_constraints.cpp
index 038b32e65..dba76efad 100644
--- a/src/kernel/universe_constraints.cpp
+++ b/src/kernel/universe_constraints.cpp
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <utility>
+#include <vector>
 #include "util/safe_arith.h"
 #include "util/pair.h"
 #include "util/buffer.h"
diff --git a/src/kernel/universe_constraints.h b/src/kernel/universe_constraints.h
index c5900188c..4ccbdb6f7 100644
--- a/src/kernel/universe_constraints.h
+++ b/src/kernel/universe_constraints.h
@@ -6,6 +6,9 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <unordered_map>
+#include <utility>
+#include <functional>
+#include <vector>
 #include "util/name.h"
 #include "util/hash.h"
 #include "util/name_map.h"
@@ -42,7 +45,7 @@ public:
     */
     bool contains(name const & n) const;
     /** \brief Return true iff n1 >= n2 + k is implied by this set of constraints. */
-    bool is_implied(name const & n1, name const & n2, int k) const ;
+    bool is_implied(name const & n1, name const & n2, int k) const;
     /** \brief Return true iff n1 < n2 + k is not implied by this set of constraints. */
     bool is_consistent(name const & n1, name const & n2, int k) const;
     /**
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index 09eaa9f69..cafb79e21 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -986,13 +986,13 @@ static int environment_parent(lua_State * L) {
     return push_environment(L, env->parent());
 }
 
-static int environment_add_uvar(lua_State * L) {
+static int environment_add_uvar_cnstr(lua_State * L) {
     rw_shared_environment env(L, 1);
     int nargs = lua_gettop(L);
     if (nargs == 2)
-        env->add_uvar(to_name_ext(L, 2));
+        env->add_uvar_cnstr(to_name_ext(L, 2));
     else
-        env->add_uvar(to_name_ext(L, 2), to_level(L, 3));
+        env->add_uvar_cnstr(to_name_ext(L, 2), to_level(L, 3));
     return 0;
 }
 
@@ -1166,7 +1166,7 @@ static const struct luaL_Reg environment_m[] = {
     {"has_parent",     safe_function<environment_has_parent>},
     {"has_children",   safe_function<environment_has_children>},
     {"parent",         safe_function<environment_parent>},
-    {"add_uvar",       safe_function<environment_add_uvar>},
+    {"add_uvar_cnstr", safe_function<environment_add_uvar_cnstr>},
     {"is_ge",          safe_function<environment_is_ge>},
     {"get_uvar",       safe_function<environment_get_uvar>},
     {"add_definition", safe_function<environment_add_definition>},
diff --git a/src/library/printer.cpp b/src/library/printer.cpp
index 5affc16a4..4383f3167 100644
--- a/src/library/printer.cpp
+++ b/src/library/printer.cpp
@@ -202,7 +202,7 @@ std::ostream & operator<<(std::ostream & out, context const & ctx) {
 std::ostream & operator<<(std::ostream & out, object const & obj) {
     out << obj.keyword() << " ";
     switch (obj.kind()) {
-    case object_kind::UVarDeclaration:
+    case object_kind::UVarConstraint:
         out << obj.get_name() << " >= " << obj.get_cnstr_level(); break;
     case object_kind::Postulate:
         out << obj.get_name() << " : " << obj.get_type(); break;
diff --git a/src/tests/frontends/lean/frontend.cpp b/src/tests/frontends/lean/frontend.cpp
index e77a6e46b..df0573b67 100644
--- a/src/tests/frontends/lean/frontend.cpp
+++ b/src/tests/frontends/lean/frontend.cpp
@@ -20,7 +20,7 @@ using namespace lean;
 
 static void tst1() {
     environment env; io_state ios = init_frontend(env);
-    env->add_uvar("tst");
+    env->add_uvar_cnstr("tst");
     environment c = env->mk_child();
     lean_assert(c->get_uvar("tst") == env->get_uvar("tst"));
     lean_assert(env->has_children());
@@ -131,7 +131,7 @@ static void tst9() {
         lean_assert(env->has_children());
     }
     lean_assert(!env->has_children());
-    env->add_uvar("l", level()+1);
+    env->add_uvar_cnstr("l", level()+1);
     lean_assert(env->get_uvar("l") == level("l"));
     try { env->get_uvar("l2"); lean_unreachable(); }
     catch (exception &) {}
diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index 91d92ee8c..b633f0b7d 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -21,8 +21,8 @@ using namespace lean;
 
 static void tst1() {
     environment env;
-    level u = env->add_uvar("u", level() + 1);
-    level w = env->add_uvar("w", u + 1);
+    level u = env->add_uvar_cnstr("u", level() + 1);
+    level w = env->add_uvar_cnstr("w", u + 1);
     lean_assert(!env->has_children());
     lean_assert(!env->has_parent());
     {
@@ -34,21 +34,21 @@ static void tst1() {
         lean_assert(child->has_parent());
         lean_assert(!env->has_parent());
         try {
-            level o = env->add_uvar("o", w + 1);
+            level o = env->add_uvar_cnstr("o", w + 1);
             lean_unreachable();
         } catch (exception const & ex) {
             std::cout << "expected error: " << ex.what() << "\n";
         }
     }
     std::cout << "tst1 checkpoint" << std::endl;
-    level o = env->add_uvar("o", w + 1);
+    level o = env->add_uvar_cnstr("o", w + 1);
     lean_assert(!env->has_children());
     std::cout << env;
 }
 
 static environment mk_child() {
     environment env;
-    level u = env->add_uvar("u", level() + 1);
+    level u = env->add_uvar_cnstr("u", level() + 1);
     return env->mk_child();
 }
 
@@ -134,8 +134,8 @@ static void tst5() {
 
 static void tst6() {
     environment env; init_test_frontend(env);
-    level u = env->add_uvar("u", level() + 1);
-    level w = env->add_uvar("w", u + 1);
+    level u = env->add_uvar_cnstr("u", level() + 1);
+    level w = env->add_uvar_cnstr("w", u + 1);
     env->add_var("f", mk_arrow(Type(u), Type(u)));
     expr t = Const("f")(Int);
     std::cout << "type of " << t << " is " << type_check(t, env) << "\n";
@@ -194,16 +194,10 @@ static void tst8() {
 }
 
 static void tst9() {
-    try {
-        environment env;
-        env->add_uvar("u1", level());
-        env->add_uvar("u2", level());
-        env->add_uvar("u1", level("u2"));
-    } catch (already_declared_exception & ex) {
-        std::cout << ex.what() << "\n";
-        level l = ex.get_environment()->get_uvar(ex.get_name());
-        std::cout << l << "\n";
-    }
+    environment env;
+    env->add_uvar_cnstr("u1", level());
+    env->add_uvar_cnstr("u2", level());
+    env->add_uvar_cnstr("u1", level("u2"));
 }
 
 static void tst10() {
diff --git a/src/tests/kernel/level.cpp b/src/tests/kernel/level.cpp
index afa1da79a..4f8c34e65 100644
--- a/src/tests/kernel/level.cpp
+++ b/src/tests/kernel/level.cpp
@@ -29,7 +29,7 @@ static void tst0() {
     std::for_each(env->begin_objects(), env->end_objects(), [&](object const & obj) {
             std::cout << obj.keyword() << "\n";
         });
-    level l1 = env->add_uvar(name(name("l1"), "suffix"), level());
+    level l1 = env->add_uvar_cnstr(name(name("l1"), "suffix"), level());
     lean_assert(env->begin_objects() != env->end_objects());
     std::for_each(env->begin_objects(), env->end_objects(), [&](object const & obj) {
             std::cout << obj.keyword() << "\n";
@@ -39,10 +39,10 @@ static void tst0() {
 
 static void tst1() {
     environment env;
-    level l1 = env->add_uvar(name(name("l1"), "suffix"), level());
-    level l2 = env->add_uvar("l2", l1 + 10);
-    level l3 = env->add_uvar("l3", max(l2, l1 + 3));
-    level l4 = env->add_uvar("l4", max(l1 + 8, max(l2 + 2, l3 + 20)));
+    level l1 = env->add_uvar_cnstr(name(name("l1"), "suffix"), level());
+    level l2 = env->add_uvar_cnstr("l2", l1 + 10);
+    level l3 = env->add_uvar_cnstr("l3", max(l2, l1 + 3));
+    level l4 = env->add_uvar_cnstr("l4", max(l1 + 8, max(l2 + 2, l3 + 20)));
     check_serializer(l1);
     check_serializer(l2);
     check_serializer(l3);
@@ -57,23 +57,17 @@ static void tst1() {
 
 static void tst2() {
     environment env;
-    level l1 = env->add_uvar("l1", level());
-    try {
-        level l2 = env->add_uvar("l1", level());
-        lean_unreachable();
-    }
-    catch (exception & ex) {
-        std::cout << "ok\n";
-    }
+    level l1 = env->add_uvar_cnstr("l1", level());
+    level l2 = env->add_uvar_cnstr("l1", level());
 }
 
 static void tst3() {
     environment env;
-    level l1 = env->add_uvar("l1", level());
-    level l2 = env->add_uvar("l2", l1 + ((1<<30) + 1024));
+    level l1 = env->add_uvar_cnstr("l1", level());
+    level l2 = env->add_uvar_cnstr("l2", l1 + ((1<<30) + 1024));
     check_serializer(l2);
     try {
-        level l3 = env->add_uvar("l3", l2 + (1<<30));
+        level l3 = env->add_uvar_cnstr("l3", l2 + (1<<30));
         lean_unreachable();
     }
     catch (exception & ex) {
@@ -83,12 +77,12 @@ static void tst3() {
 
 static void tst4() {
     environment env;
-    level l1 = env->add_uvar("l1", level() + 1);
-    level l2 = env->add_uvar("l2", level() + 1);
-    level l3 = env->add_uvar("l3", max(l1, l2) + 1);
-    level l4 = env->add_uvar("l4", l3 + 1);
-    level l5 = env->add_uvar("l5", l3 + 1);
-    level l6 = env->add_uvar("l6", max(l4, l5) + 1);
+    level l1 = env->add_uvar_cnstr("l1", level() + 1);
+    level l2 = env->add_uvar_cnstr("l2", level() + 1);
+    level l3 = env->add_uvar_cnstr("l3", max(l1, l2) + 1);
+    level l4 = env->add_uvar_cnstr("l4", l3 + 1);
+    level l5 = env->add_uvar_cnstr("l5", l3 + 1);
+    level l6 = env->add_uvar_cnstr("l6", max(l4, l5) + 1);
     check_serializer(l1);
     check_serializer(l2);
     check_serializer(l3);
@@ -117,8 +111,8 @@ static void tst4() {
 
 static void tst5() {
     environment env;
-    level l1 = env->add_uvar("l1", level() + 1);
-    level l2 = env->add_uvar("l2", level() + 1);
+    level l1 = env->add_uvar_cnstr("l1", level() + 1);
+    level l2 = env->add_uvar_cnstr("l2", level() + 1);
     std::cout << max(l1, l1) << "\n";
     lean_assert(max(l1, l1) == l1);
     lean_assert(max(l1+1, l1+1) == l1+1);
diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp
index a42ef4170..ebb2bbdbe 100644
--- a/src/tests/kernel/type_checker.cpp
+++ b/src/tests/kernel/type_checker.cpp
@@ -36,8 +36,8 @@ static void tst1() {
     expr f = mk_pi("_", t0, t0);
     std::cout << type_check(f, env) << "\n";
     lean_assert(type_check(f, env) == Type(level()+1));
-    level u = env->add_uvar("u", level() + 1);
-    level v = env->add_uvar("v", level() + 1);
+    level u = env->add_uvar_cnstr("u", level() + 1);
+    level v = env->add_uvar_cnstr("v", level() + 1);
     expr g = mk_pi("_", Type(u), Type(v));
     std::cout << type_check(g, env) << "\n";
     lean_assert(type_check(g, env) == Type(max(u+1, v+1)));
@@ -59,7 +59,7 @@ static void tst1() {
 static void tst2() {
     try{
         environment env;
-        level l1      = env->add_uvar("l1", level() + 1);
+        level l1      = env->add_uvar_cnstr("l1", level() + 1);
         expr t0       = Type();
         expr t1       = Type(l1);
         expr F =
diff --git a/tests/lua/env1.lua b/tests/lua/env1.lua
index 508eafe08..d0d2087b3 100644
--- a/tests/lua/env1.lua
+++ b/tests/lua/env1.lua
@@ -1,7 +1,7 @@
 import("util.lua")
 e = environment()
 assert(is_environment(e))
-e:add_uvar("M1")
+e:add_uvar_cnstr("M1")
 print(e:get_uvar("M1"))
 e:add_var("N", Type())
 N, M = Consts("N M")
diff --git a/tests/lua/env4.lua b/tests/lua/env4.lua
index d2323b8f7..06df329ff 100644
--- a/tests/lua/env4.lua
+++ b/tests/lua/env4.lua
@@ -1,7 +1,7 @@
 assert(not pcall(function() get_environment() end))
 local env = environment()
 env:import("Int")
-env:add_uvar("Z", level(level("M"), 1))
+env:add_uvar_cnstr("Z", level(level("M"), 1))
 assert(env:is_ge(level("Z"), level("M")))
 local child = env:mk_child()
 assert(env:has_children())
@@ -16,7 +16,9 @@ print(not eenv:find_object("Int"))
 assert(not pcall(function() env:parent() end))
 local p = child:parent()
 assert(p:has_children())
-assert(not pcall(function() env:add_uvar("Z") end))
+assert(not pcall(function() env:add_uvar_cnstr("Z") end))
+child:add_uvar_cnstr("Z")
+assert(not pcall(function() child:add_uvar_cnstr("M", level("Z")) end))
 child:add_definition("val1", Const("true"), true)
 child:add_definition("val2", Const("Bool"), Const("true"), true)
 local ok, msg = pcall(function() child:add_definition("val3", Const("Int"), Const("true"), true) end)