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

chore(library/attribute_manager): fix warning

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-05 17:22:01 -07:00
parent 15595c0061
commit 38524475c9
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/attribute_manager.h
View file

@ -85,8 +85,9 @@ private:
protected:
virtual void write_entry(serializer &, attr_data const &) const override final {}
virtual attr_data_ptr read_entry(deserializer &) const override final { return attr_data_ptr(new attr_data); }
virtual environment set_untyped(environment const & env, io_state const & ios, name const & n, attr_data_ptr data,
bool persistent) const override final {
virtual environment set_untyped(environment const & /*env */, io_state const & /* ios */,
name const & /* n */, attr_data_ptr /* data */,
bool /* persistent */) const override final {
// TODO(sullrich): Use priority from `data` as soon as available
lean_unreachable();
}