diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index a4095487aad9..ce07129b45f9 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -592,7 +592,7 @@ mutual
           to this application rather than sometimes being placed at position (1,0) in the file.
           Placing position information on `by` syntax alone is not sufficient since incrementality
           (in particular, `Lean.Elab.Term.withReuseContext`) controls the ref to avoid leakage of outside data.
-          Note that `tacticSyntax` contains no position information.
+          Note that `tacticSyntax` contains no position information itself, since it is erased by `Lean.Elab.Term.quoteAutoTactic`.
           -/
           let info := (← getRef).getHeadInfo
           let tacticBlock := tacticBlock.raw.rewriteBottomUp (·.setInfo info)
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index f3b4881c8a81..cc4706f234ce 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -678,7 +678,7 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
             | .ok tacticSyntax =>
               let stx ← `(by $tacticSyntax)
               -- See comment in `Lean.Elab.Term.ElabAppArgs.processExplicitArg` about `tacticSyntax`.
-              -- Adding info for reliable positions for messages.
+              -- We add info to get reliable positions for messages from evaluating the tactic script.
               let info := field.ref.getHeadInfo
               let stx := stx.raw.rewriteBottomUp (·.setInfo info)
               cont (← elabTermEnsuringType stx (d.getArg! 0).consumeTypeAnnotations) field