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

chore(frontends/lean/notation_cmd): cleanup weird coding pattern

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-13 17:27:25 -08:00
parent 912c5254de
commit 1048812e2e
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/notation_cmd.cpp
View file

@ -252,9 +252,9 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota
case mixfix_kind::infixl:
#if defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
#endif
return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec), pp_tk)),
mk_app(f, Var(1), Var(0)), overload, priority, grp, parse_only), new_token);
#endif
case mixfix_kind::infixr:
return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec), pp_tk)),
mk_app(f, Var(1), Var(0)), overload, priority, grp, parse_only), new_token);