From 0bc101ac2860157a63cc0eca8a344e3afcf27a86 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 May 2014 15:28:34 -0700 Subject: [PATCH] fix(kernel/metavar): typo Signed-off-by: Leonardo de Moura --- src/kernel/metavar.cpp | 2 +- src/kernel/metavar.h | 4 ---- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 7883406439..ddd6864c3a 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -94,7 +94,7 @@ substitution substitution::assign(name const & m, level const & l) const { } std::pair substitution::d_instantiate_metavars(level const & l, bool use_jst, bool updt) { - if (!has_param(l)) + if (!has_meta(l)) return mk_pair(l, justification()); justification j; auto save_jst = [&](justification const & j2) { j = mk_composite1(j, j2); }; diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index 7bb8a961da..2ddb8156df 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -96,10 +96,6 @@ public: /** \brief Return true iff the metavariable \c m occurrs (directly or indirectly) in \c e. */ bool occurs_expr(name const & m, expr const & e) const; - /** \brief Return true iff the meta universe parameter \c m occurrs (directly or indirectly) in \c e. */ - bool occurs_level(name const & m, expr const & e) const; - bool occurs(expr const & m, expr const & e) const { lean_assert(is_metavar(m)); return occurs_expr(mlocal_name(m), e); } - bool occurs(level const & m, expr const & e) const { lean_assert(is_meta(m)); return occurs_expr(meta_id(m), e); } }; }