From dd5b221d32676c8104c42dd912301fb3a02fc332 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 May 2015 09:42:32 -0700 Subject: [PATCH] fix(library/user_recursors): warning message --- src/library/user_recursors.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index 4a85ea4ecc..e7148f2bfc 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -106,12 +106,13 @@ recursor_info mk_recursor_info(environment const & env, name const & r) { "motive result sort must be Type.{l} where l is a universe parameter"); } name l = param_id(C_lvl); - C_univ_pos = 0; + unsigned uni_pos = 0; for (name const & l_curr : d.get_univ_params()) { if (l_curr == l) break; - C_univ_pos = *C_univ_pos + 1; + uni_pos++; } + C_univ_pos = uni_pos; lean_assert(*C_univ_pos < length(d.get_univ_params())); }