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

fix(library/user_recursors): warning

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-13 10:04:38 -07:00
parent dd5b221d32
commit d0582b2537
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/user_recursors.cpp
View file

@ -94,6 +94,10 @@ recursor_info mk_recursor_info(environment const & env, name const & r) {
if (!is_sort(C_rtype) || C_tele.size() != C_args.size()) {
throw_invalid_motive(C);
}
// The following pragma is for avoiding gcc bogus warning
#if defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
#endif
optional<unsigned> C_univ_pos;
level C_lvl = sort_level(C_rtype);
if (!is_standard(env) || !is_zero(C_lvl)) {