From c096eec1d6f090173f6b964ab5ba1f4383126441 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Jan 2014 17:09:04 -0800 Subject: [PATCH] chore(kernel/expr): remove dead code Signed-off-by: Leonardo de Moura --- src/kernel/expr.cpp | 12 +----------- src/kernel/expr.h | 2 -- 2 files changed, 1 insertion(+), 13 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index ec74121b5..ed9d44614 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -279,16 +279,6 @@ bool is_arrow(expr const & t) { } } -bool is_heq(expr const & e, expr & lhs, expr & rhs) { - if (is_heq(e)) { - lhs = heq_lhs(e); - rhs = heq_rhs(e); - return true; - } else { - return false; - } -} - expr copy(expr const & a) { switch (a.kind()) { case expr_kind::Var: return mk_var(var_idx(a)); @@ -465,7 +455,7 @@ public: name n = read_name(d); return mk_metavar(n, read_local_context(d)); }} - throw_corrupted_file(); + throw_corrupted_file(); // LCOV_EXCL_LINE }); } }; diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 79b7e2c03..49fc00971 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -544,8 +544,6 @@ inline name const & metavar_name(expr const & e) { return to_metavar(e) inline local_context const & metavar_lctx(expr const & e) { return to_metavar(e)->get_lctx(); } inline bool has_metavar(expr const & e) { return e.has_metavar(); } - -bool is_heq(expr const & e, expr & lhs, expr & rhs); // ======================================= // =======================================