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

chore(frontends/lean/parser): remove dead variable

Browse source
This commit is contained in:
Leonardo de Moura 2017-02-03 19:55:19 -08:00
parent 01414cf21c
commit 91b68b6b90
2 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/parser.cpp
View file

@ -158,7 +158,7 @@ parser::parser(environment const & env, io_state const & ios,
std::istream & strm, std::string const & file_name,
bool use_exceptions,
std::shared_ptr<snapshot const> const & s, snapshot_vector * sv):
m_env(env), m_ios(ios), m_verbose(true),
m_env(env), m_ios(ios),
m_use_exceptions(use_exceptions),
m_import_fn(import_fn),
m_file_name(file_name),
@ -264,7 +264,6 @@ void parser::declare_sorry_if_used() {
}
void parser::updt_options() {
m_verbose = get_verbose(m_ios.get_options());
m_show_errors = get_parser_show_errors(m_ios.get_options());
}

1
src/frontends/lean/parser.h
View file

@ -125,7 +125,6 @@ enum class id_behavior {
class parser : public abstract_parser {
environment m_env;
io_state m_ios;
bool m_verbose;
bool m_use_exceptions;
bool m_show_errors;
module_loader m_import_fn;