From 3feae112bc181ec4d888083cd1d579d669a6ba32 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 11 Sep 2018 13:55:03 -0700 Subject: [PATCH] chore(frontends/lean/parser): unused var warning --- src/frontends/lean/parser.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 260a1d1f74..011293fa21 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -2193,7 +2193,6 @@ void parser::parse_imports(std::vector & imports) { while (true) { bool k_init = false; unsigned k = 0; - unsigned h = 0; while (true) { if (curr_is_token(get_period_tk()) || curr_is_token(get_dotdot_tk()) || curr_is_token(get_ellipsis_tk())) { @@ -2201,10 +2200,8 @@ void parser::parse_imports(std::vector & imports) { if (!k_init) { k = d - 1; k_init = true; - h = d - 1; } else { k = d; - h = d; } next(); } else {