From d54a67cf2e0be63d4704a310f8d481d300f52430 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 1 Mar 2016 17:50:28 -0800 Subject: [PATCH] fix(library): compilation warnings on OSX --- src/library/blast/blast.cpp | 4 ++-- src/library/type_context.h | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index b364c42a31..1fabe0f29c 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -1458,7 +1458,7 @@ public: /** \brief Return the type of a local constant (local or not). \remark This method allows the customer to store the type of local constants in a different place. */ - virtual expr infer_local(expr const & e) const { + virtual expr infer_local(expr const & e) const override { state const & s = curr_state(); if (is_href(e)) { hypothesis const & h = s.get_hypothesis_decl(e); @@ -1468,7 +1468,7 @@ public: } } - virtual expr infer_metavar(expr const & m) const { + virtual expr infer_metavar(expr const & m) const override { if (is_mref(m)) { state const & s = curr_state(); metavar_decl const * d = s.get_metavar_decl(m); diff --git a/src/library/type_context.h b/src/library/type_context.h index d167c62bce..cfb3e82dca 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -310,7 +310,7 @@ public: void set_local_instances(list const & insts); - environment const & env() const { return m_env; } + virtual environment const & env() const override { return m_env; } /** \brief Opaque constants are never unfolded by this procedure. The is_def_eq method will lazily unfold non-opaque constants. @@ -450,7 +450,7 @@ public: bool is_prop(expr const & e); /** \brief Infer the type of \c e. */ - expr infer(expr const & e); + virtual expr infer(expr const & e) override; /** \brief Put \c e in whnf, it is a Pi, then return whnf, otherwise return e */ expr try_to_pi(expr const & e);