diff --git a/src/Lean/Elab/Tactic/Location.lean b/src/Lean/Elab/Tactic/Location.lean
index 6276f584ca..45c630920c 100644
--- a/src/Lean/Elab/Tactic/Location.lean
+++ b/src/Lean/Elab/Tactic/Location.lean
@@ -39,9 +39,16 @@ def expandOptLocation (stx : Syntax) : Location :=
 
 open Meta
 
-/-- Runs the given `atLocal` and `atTarget` methods on each of the locations selected by the given `loc`.
-If any of the selected tactic applications fail, it will call `failed` with the main goal mvar.
- -/
+/--
+Runs the given `atLocal` and `atTarget` methods on each of the locations selected by the given `loc`.
+
+* If `loc` is a list of locations, runs at each specified hypothesis (and finally the goal if `⊢` is included),
+  and fails if any of the tactic applications fail.
+* If `loc` is `*`, runs at the target first and then the hypotheses in reverse order.
+  If all tactic applications fail, `withLocation` with call `failed` with the main goal mvar.
+  If the tactic application closes the main goal, `withLocation` will then fail with `no goals to be solved`
+  upon reaching the first hypothesis.
+-/
 def withLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget : TacticM Unit) (failed : MVarId → TacticM Unit) : TacticM Unit := do
   match loc with
   | Location.targets hyps type =>