max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/type_context): fix compilation warning

Browse source
This commit is contained in:
Leonardo de Moura 2018-02-07 09:42:24 -08:00
parent 21e52408b2
commit e06c3cbd8f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/type_context.h
View file

@ -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; }