diff --git a/src/kernel/error_msgs.cpp b/src/kernel/error_msgs.cpp
index 2e70d4606..4e3739438 100644
--- a/src/kernel/error_msgs.cpp
+++ b/src/kernel/error_msgs.cpp
@@ -19,10 +19,6 @@ format pp_function_expected(formatter const & fmt, options const & opts, expr co
     return compose(format("function expected at"), pp_indent_expr(fmt, opts, e));
 }
 
-format pp_pair_expected(formatter const & fmt, options const & opts, expr const & e) {
-    return compose(format("pair expected at"), pp_indent_expr(fmt, opts, e));
-}
-
 format pp_app_type_mismatch(formatter const & fmt, options const & opts, expr const & app,
                             expr const & expected_type, expr const & given_type) {
     format r;
@@ -35,16 +31,6 @@ format pp_app_type_mismatch(formatter const & fmt, options const & opts, expr co
     return r;
 }
 
-format pp_proj_type_mismatch(formatter const & fmt, options const & opts, expr const & proj,
-                             expr const & arg_type) {
-    format r;
-    r += format("type mismatch at projection");
-    r += pp_indent_expr(fmt, opts, proj);
-    r += format("pair expected, given type:");
-    r += pp_indent_expr(fmt, opts, arg_type);
-    return r;
-}
-
 format pp_def_type_mismatch(formatter const & fmt, options const & opts, name const & n,
                             expr const & expected_type, expr const & given_type) {
     format r("type mismatch at definition '");
@@ -55,4 +41,11 @@ format pp_def_type_mismatch(formatter const & fmt, options const & opts, name co
     r += pp_indent_expr(fmt, opts, given_type);
     return r;
 }
+format pp_def_lvl_cnstrs_satisfied(formatter const & fmt, options const & opts, expr const & e, level const & lhs, level const & rhs) {
+    format r("constand definition level constraints are not satisfied");
+    r += pp_indent_expr(fmt, opts, e);
+    r += format("level constraint:");
+    r += pp(lhs, rhs, opts);
+    return r;
+}
 }
diff --git a/src/kernel/error_msgs.h b/src/kernel/error_msgs.h
index a8bd4c473..b24b1f63e 100644
--- a/src/kernel/error_msgs.h
+++ b/src/kernel/error_msgs.h
@@ -10,11 +10,9 @@ Author: Leonardo de Moura
 namespace lean {
 format pp_type_expected(formatter const & fmt, options const & opts, expr const & e);
 format pp_function_expected(formatter const & fmt, options const & opts, expr const & e);
-format pp_pair_expected(formatter const & fmt, options const & opts, expr const & e);
 format pp_app_type_mismatch(formatter const & fmt, options const & opts, expr const & app,
                             expr const & expected_type, expr const & given_type);
-format pp_proj_type_mismatch(formatter const & fmt, options const & opts, expr const & proj,
-                             expr const & arg_type);
 format pp_def_type_mismatch(formatter const & fmt, options const & opts, name const & n,
                             expr const & expected_type, expr const & given_type);
+format pp_def_lvl_cnstrs_satisfied(formatter const & fmt, options const & opts, expr const & e, level const & lhs, level const & rhs);
 }