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

chore(library/module): remove dead declaration

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-14 07:51:44 -07:00
parent 22d2848d21
commit e616def866
2 changed files with 2 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/module.cpp
View file

@ -287,6 +287,8 @@ static olean_data parse_olean(std::istream & in, std::string const & file_name,
return { imports, code };
}
using modification_list = std::vector<modification*>;
static void import_module(modification_list const & modifications, environment & env) {
for (auto & m : modifications) {
m->perform(env);

11
src/library/module.h
View file

@ -29,17 +29,6 @@ environment import_modules(unsigned trust_lvl, std::vector<module_name> const &
/** \brief Store module using \c env. */
void write_module(environment const & env, module_name const & mod, std::string const & olean_fn);
struct modification;
using modification_list = std::vector<modification*>;
/** \brief A finished module. The in-memory representation of a .olean file. */
struct loaded_module {
module_name m_name; // not serialized
std::vector<module_name> m_imports;
modification_list m_modifications;
};
struct modification {
public:
virtual ~modification() {}