From e06c3cbd8fb91d739312453c734bf4b33535335a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 Feb 2018 09:42:24 -0800 Subject: [PATCH] chore(library/type_context): fix compilation warning --- src/library/type_context.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/type_context.h b/src/library/type_context.h index 05a8e02abb..25f07c47d5 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -714,7 +714,7 @@ public: virtual environment const & env() const override { return m_cache->m_env; } // TODO(Leo): avoid ::lean::mk_fresh_name - virtual name mk_fresh_name() { return ::lean::mk_fresh_name(); } + virtual name mk_fresh_name() override { return ::lean::mk_fresh_name(); } options const & get_options() const { return m_cache->m_options; } local_context const & lctx() const { return m_lctx; }