From 91e8f0b8fac673e35e7e3799a76e0df39314feac Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Jul 2014 16:37:55 +0100
Subject: [PATCH] chore(frontends/lean/elaborator): replace ... withe exception

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/elaborator.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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<constraints>();
         }