diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index f4fc7b7b24..bf1ecabf0f 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -342,12 +342,11 @@ level environment_cell::add_uvar_cnstr(name const & n, level const & l) {
     check_consistency(n, l, 0);
     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.
         r = *it;
-        m_objects.push_back(mk_uvar_cnstr(n, l));
     }
+    m_objects.push_back(mk_uvar_cnstr(n, l));
     add_constraints(n, l, 0);
     return r;
 }
diff --git a/tests/lean/lua11.lean b/tests/lean/lua11.lean
index ff70caccce..0f6f2247be 100644
--- a/tests/lean/lua11.lean
+++ b/tests/lean/lua11.lean
@@ -30,20 +30,12 @@ import Int.
  assert(found2)
  print(bs)
  assert(not bs:in_builtin_set(Const("a")))
- assert(not pcall(function() M:in_builtin_set(Const("a")) end))
 
- local M   = env:find_object("M")
- assert(not M:has_type())
- assert(not pcall(function() M:get_type() end))
- assert(M:has_cnstr_level())
- print(M:get_cnstr_level())
  assert(not pcall(function() o1:get_cnstr_level() end))
- assert(not pcall(function() M:get_value() end))
  env:add_var("x", Const("Int"))
  env:add_definition("val", Const("Int"), Const("x"))
  assert(env:find_object("val"):get_value() == Const("x"))
  assert(env:find_object("val"):get_weight() == 1)
- assert(not pcall(function() M:get_weight() end))
  assert(env:find_object("congr"):is_opaque())
  assert(env:find_object("congr"):is_theorem())
  assert(env:find_object("refl"):is_axiom())
diff --git a/tests/lean/lua11.lean.expected.out b/tests/lean/lua11.lean.expected.out
index 8ea9e72310..039d56af98 100644
--- a/tests/lean/lua11.lean.expected.out
+++ b/tests/lean/lua11.lean.expected.out
@@ -3,4 +3,3 @@
   Imported 'Int'
 Int::add
 builtinset Nat::numeral
-512
diff --git a/tests/lean/univ3.lean b/tests/lean/univ3.lean
new file mode 100644
index 0000000000..31a3cf0df9
--- /dev/null
+++ b/tests/lean/univ3.lean
@@ -0,0 +1,7 @@
+universe Z >= 0
+definition Z := 0
+eval Z
+definition TZ := (Type Z)
+eval TZ
+definition U := 1
+eval U
\ No newline at end of file
diff --git a/tests/lean/univ3.lean.expected.out b/tests/lean/univ3.lean.expected.out
new file mode 100644
index 0000000000..27a747cefa
--- /dev/null
+++ b/tests/lean/univ3.lean.expected.out
@@ -0,0 +1,8 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Defined: Z
+0
+  Defined: TZ
+(Type Z)
+  Defined: U
+1