From 390a78a8d2d22caf2d812e2c4bcfdaad277fe8db Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Dec 2013 15:35:12 -0800 Subject: [PATCH] chore(frontends/lean/parser): remove 'Skipped' message Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 7 ++----- tests/lean/mod1.lean.expected.out | 2 -- 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index ae49020bf..bc57fc254 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -2453,11 +2453,8 @@ class parser::imp { } else { r = m_env->import(fname, m_io_state); } - if (m_verbose) { - if (r) - regular(m_io_state) << " Imported '" << fname << "'" << endl; - else - regular(m_io_state) << " Skipped '" << fname << "'" << endl; + if (m_verbose && r) { + regular(m_io_state) << " Imported '" << fname << "'" << endl; } } diff --git a/tests/lean/mod1.lean.expected.out b/tests/lean/mod1.lean.expected.out index ecb382647..c51516045 100644 --- a/tests/lean/mod1.lean.expected.out +++ b/tests/lean/mod1.lean.expected.out @@ -1,8 +1,6 @@ Set: pp::colors Set: pp::unicode Imported 'cast' - Skipped 'cast' Imported 'cast' - Skipped 'cast' @cast : Π (A B : (Type U)), A == B → A → B @cast : Π (A B : (Type U)), A == B → A → B