From 010338cb183f9329eddee3aa9a5578e45d18d923 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 17 Feb 2021 11:52:22 +0100
Subject: [PATCH] chore: improve "no elaborator" error message

---
 src/Lean/Elab/Term.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index c9c5c6230c..33b495fde8 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -909,7 +909,7 @@ private def elabUsingElabFns (stx : Syntax) (expectedType? : Option Expr) (catch
   let k := stx.getKind
   match table.find? k with
   | some elabFns => elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns
-  | none         => throwError! "elaboration function for '{k}' has not been implemented"
+  | none         => throwError! "elaboration function for '{k}' has not been implemented{indentD stx}"
 
 instance : MonadMacroAdapter TermElabM where
   getCurrMacroScope := getCurrMacroScope