modify comments

leanprover · Aug 6, 2024 · d7a4b80 · d7a4b80
1 parent 8af4d46
commit d7a4b80
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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