michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/type_context): compilation warning

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-05 16:32:59 -08:00
parent 8d9d84f33c
commit 7e7919950d
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/type_context.h
View file

@ -22,6 +22,7 @@ class tmp_local_generator {
name mk_fresh_name(); name mk_fresh_name();
public: public:
tmp_local_generator(); tmp_local_generator();
virtual ~tmp_local_generator() {}
/** \brief Create a temporary local constant */ /** \brief Create a temporary local constant */
virtual expr mk_tmp_local(expr const & type, binder_info const & bi); virtual expr mk_tmp_local(expr const & type, binder_info const & bi);