diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 87688b081..427835fd8 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -2255,8 +2255,6 @@ class parser::imp { return; } try { - if (m_verbose) - regular(m_io_state) << "Importing file '" << fname << "'" << endl; parser import_parser(m_env, m_io_state, in, m_script_state, true /* use exceptions */, false /* not interactive */); import_parser(); } catch (interrupted &) { diff --git a/tests/lean/cast1.lean.expected.out b/tests/lean/cast1.lean.expected.out index 071b3a5b8..0702123ea 100644 --- a/tests/lean/cast1.lean.expected.out +++ b/tests/lean/cast1.lean.expected.out @@ -1,6 +1,5 @@ Set: pp::colors Set: pp::unicode -Importing file '/home/leo/projects/lean/build/debug/shell/cast.lean' Assumed: cast Assumed: CastEq Assumed: CastApp diff --git a/tests/lean/cast2.lean.expected.out b/tests/lean/cast2.lean.expected.out index d77e315c6..73bc1a18f 100644 --- a/tests/lean/cast2.lean.expected.out +++ b/tests/lean/cast2.lean.expected.out @@ -1,6 +1,5 @@ Set: pp::colors Set: pp::unicode -Importing file '/home/leo/projects/lean/build/debug/shell/cast.lean' Assumed: cast Assumed: CastEq Assumed: CastApp diff --git a/tests/lean/cast3.lean.expected.out b/tests/lean/cast3.lean.expected.out index 262f76431..0b2c56e9c 100644 --- a/tests/lean/cast3.lean.expected.out +++ b/tests/lean/cast3.lean.expected.out @@ -1,6 +1,5 @@ Set: pp::colors Set: pp::unicode -Importing file '/home/leo/projects/lean/build/debug/shell/cast.lean' Assumed: cast Assumed: CastEq Assumed: CastApp diff --git a/tests/lean/cast4.lean.expected.out b/tests/lean/cast4.lean.expected.out index 5f1d29d3c..59f4e9d90 100644 --- a/tests/lean/cast4.lean.expected.out +++ b/tests/lean/cast4.lean.expected.out @@ -1,6 +1,5 @@ Set: pp::colors Set: pp::unicode -Importing file '/home/leo/projects/lean/build/debug/shell/cast.lean' Assumed: cast Assumed: CastEq Assumed: CastApp diff --git a/tests/lean/mod1.lean.expected.out b/tests/lean/mod1.lean.expected.out index dbeb12192..f5a3e3192 100644 --- a/tests/lean/mod1.lean.expected.out +++ b/tests/lean/mod1.lean.expected.out @@ -1,9 +1,7 @@ Set: pp::colors Set: pp::unicode -Importing file './simple.lean' Assumed: x Assumed: y -Importing file './simple.lean' Assumed: x Assumed: y x + y : ℤ diff --git a/tests/lean/norm_bug1.lean.expected.out b/tests/lean/norm_bug1.lean.expected.out index 49f2f218f..b0d3c6bdd 100644 --- a/tests/lean/norm_bug1.lean.expected.out +++ b/tests/lean/norm_bug1.lean.expected.out @@ -1,6 +1,5 @@ Set: pp::colors Set: pp::unicode -Importing file '/home/leo/projects/lean/build/debug/shell/cast.lean' Assumed: cast Assumed: CastEq Assumed: CastApp diff --git a/tests/lean/type_inf_bug1.lean.expected.out b/tests/lean/type_inf_bug1.lean.expected.out index 65e2228e8..4cdca5f3d 100644 --- a/tests/lean/type_inf_bug1.lean.expected.out +++ b/tests/lean/type_inf_bug1.lean.expected.out @@ -1,6 +1,5 @@ Set: pp::colors Set: pp::unicode -Importing file '/home/leo/projects/lean/build/debug/shell/cast.lean' Assumed: cast Assumed: CastEq Assumed: CastApp