From 1e8a4d1da520987f223592f0389fa10abb2e18b1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 23 Oct 2020 06:15:29 -0700
Subject: [PATCH] chore: avoid useless `failed to synthesize CoeFun ...` tail
 message

---
 src/Lean/Elab/App.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index daf7276d86..3ae7991e37 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -63,9 +63,9 @@ private def tryCoeFun (α : Expr) (a : Expr) : TermElabM Expr := do
   let synthesized ←
     try
       withoutMacroStackAtErr $ synthesizeInstMVarCore mvarId
-    catch
-      | Exception.error _ msg => throwError! "function expected\n{msg}"
-      | _                     => throwError "function expected"
+    catch _ =>
+      -- Should we add an option for showing the type class failure?
+      throwError "function expected"
   if synthesized then
     pure $ mkAppN (Lean.mkConst `coeFun [u, v]) #[α, γ, a, mvar]
   else