From a608532fd460403e73fae47fdb3ed5a73637a653 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 20 Oct 2022 00:12:26 +0200
Subject: [PATCH] chore: Improve LCNF check goto error message

---
 src/Lean/Compiler/LCNF/Check.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/LCNF/Check.lean b/src/Lean/Compiler/LCNF/Check.lean
index 695c1cd814..d78c6c37c6 100644
--- a/src/Lean/Compiler/LCNF/Check.lean
+++ b/src/Lean/Compiler/LCNF/Check.lean
@@ -238,7 +238,7 @@ partial def check (code : Code) : CheckM Unit := do
     checkJpInScope fvarId
     let decl ← getFunDecl fvarId
     unless decl.getArity == args.size do
-      throwError "invalid LCNF `jmp`, join point has #{decl.getArity} parameters, but #{args.size} were provided"
+      throwError "invalid LCNF `goto`, join point {decl.binderName} has #{decl.getArity} parameters, but #{args.size} were provided"
     checkAppArgs (.fvar fvarId) args
   | .return fvarId => checkFVar fvarId
   | .unreach .. => pure ()