From 1ce3b83d7943537eb5730c84ad3f0d9393788a4e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Oct 2014 17:22:25 -0700 Subject: [PATCH] fix(kernel/metavar): compilation error in some compilers --- src/kernel/metavar.cpp | 2 +- src/kernel/metavar.h | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 40f9763c2..cd14e775e 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -337,7 +337,7 @@ name_set substitution::get_occs(name const & m, name_set & fresh) { } } -bool substitution::occurs_expr(name const & m, expr const & e) const { +bool substitution::occurs_expr(name const & m, expr const & e) { if (!has_expr_metavar(e)) return false; name_set fresh; diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index fb06669fa..882555dd7 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -105,7 +105,7 @@ public: optional get_level(level const & m) const { lean_assert(is_meta(m)); return get_level(meta_id(m)); } /** \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; - bool occurs(expr const & m, expr const & e) const { lean_assert(is_metavar(m)); return occurs_expr(mlocal_name(m), e); } + bool occurs_expr(name const & m, expr const & e); + bool occurs(expr const & m, expr const & e) { lean_assert(is_metavar(m)); return occurs_expr(mlocal_name(m), e); } }; }