From a45dc0bb86dd47627254b76877ad055735d6e39e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 21 May 2014 15:46:17 -0700
Subject: [PATCH] chore(kernel): remove dead code, we don't have level
 constraints anymore

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/error_msgs.cpp   |  8 --------
 src/kernel/error_msgs.h     |  2 --
 src/kernel/type_checker.cpp | 12 ------------
 3 files changed, 22 deletions(-)

diff --git a/src/kernel/error_msgs.cpp b/src/kernel/error_msgs.cpp
index d78b315b0..8b282b614 100644
--- a/src/kernel/error_msgs.cpp
+++ b/src/kernel/error_msgs.cpp
@@ -41,12 +41,4 @@ format pp_def_type_mismatch(formatter const & fmt, environment const & env, opti
     r += pp_indent_expr(fmt, env, opts, given_type);
     return r;
 }
-format pp_def_lvl_cnstrs_satisfied(formatter const & fmt, environment const & env, 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, env, 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 a4d1ce43a..a2ec5eaa7 100644
--- a/src/kernel/error_msgs.h
+++ b/src/kernel/error_msgs.h
@@ -15,6 +15,4 @@ format pp_app_type_mismatch(formatter const & fmt, environment const & env, opti
                             expr const & expected_type, expr const & given_type);
 format pp_def_type_mismatch(formatter const & fmt, environment const & env, options const & opts, name const & n,
                             expr const & expected_type, expr const & given_type);
-format pp_def_lvl_cnstrs_satisfied(formatter const & fmt, environment const & env, options const & opts, expr const & e,
-                                   level const & lhs, level const & rhs);
 }
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 401fc5220..f984c65fc 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -219,18 +219,6 @@ struct type_checker::imp {
         }
     }
 
-    /** \brief Create a justification for the level constraint <tt>lhs <= rhs</tt> associated with constanc \c c. */
-    justification mk_lvl_cnstr_jst(expr const & c, level const & lhs, level const & rhs) {
-        lean_assert(is_constant(c));
-        return mk_justification(c,
-                                [=](formatter const & fmt, options const & o, substitution const & subst) {
-                                    return pp_def_lvl_cnstrs_satisfied(fmt, m_env, o,
-                                                                       subst.instantiate_metavars_wo_jst(c),
-                                                                       subst.instantiate_metavars_wo_jst(lhs),
-                                                                       subst.instantiate_metavars_wo_jst(rhs));
-                                });
-    }
-
     /**
         \brief Create a justification for a application type mismatch,
         \c e is the application, \c fn_type and \c arg_type are the function and argument type.