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

chore(frontends/lean/decl_cmds): dead var

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-05 10:22:07 -07:00
parent 3a4a052167
commit 6114e00cea
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/frontends/lean/decl_cmds.cpp
View file

@ -531,7 +531,6 @@ static environment attribute_cmd_core(parser & p, bool persistent) {
return modifiers_cmd(p, {attributes, {}, {}});
}
do {
auto pos = p.pos();
name d = p.check_constant_next("invalid 'attribute' command, constant expected");
ds.push_back(d);
} while (p.curr_is_identifier());