diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 1c122682e..edc8e968d 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -355,7 +355,7 @@ class elaborator { m_tactic_result = tac(m_elab.m_env, m_elab.m_ios, ps); if (auto cs = get_next_tactic_result()) return cs; - } catch (...) {} + } catch (exception &) {} } return optional(); }