fix: Syntax.unsetTrailing (#5170)

Fixes #4958 (cherry picked from commit dcdbb9b)
leanprover · Aug 26, 2024 · d017635 · d017635
1 parent b8aefe3
commit d017635
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
@@ -388,9 +388,9 @@ def getSubstring? (stx : Syntax) (withLeading := true) (withTrailing := true) :
 partial def setTailInfoAux (info : SourceInfo) : Syntax → Option Syntax
   | atom _ val             => some <| atom info val
   | ident _ rawVal val pre => some <| ident info rawVal val pre
-  | node info k args       =>
+  | node info' k args      =>
     match updateLast args (setTailInfoAux info) args.size with
-    | some args => some <| node info k args
+    | some args => some <| node info' k args
     | none      => none
   | _                      => none