diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 309780fa67..b8bb6d4b9e 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1950,7 +1950,7 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType? if let some (e, projs) ← resolveLocalName n then unless explicitLevels.isEmpty do - throwError "invalid use of explicit universe parameters, '{e}' is a local" + throwError "invalid use of explicit universe parameters, '{e}' is a local variable" return [(e, projs)] let preresolved := preresolved.filterMap fun | .decl n projs => some (n, projs)