diff --git a/tests/tactics.v b/tests/tactics.v
index c2170c89a735642f69540f7046de55722c1cfaa8..29e27969dc595e2b2f8e32eafb1439e8becf52b3 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -51,3 +51,6 @@ Qed.
 
 Goal ∀ (n : nat), ∃ m : nat, True.
 Proof. intros ?. rename select nat into m. exists m. done. Qed.
+
+Goal ∀ (P : nat → Prop), P 3 → P 4 → P 4.
+Proof. intros. rename select (P _) into HP4. apply HP4. Qed.
diff --git a/theories/tactics.v b/theories/tactics.v
index cc9db99bc306da1323cea35b1023174c76444e03..203aa30b9008a9cc5e98cec4ed62e94409a0d0dd 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -508,14 +508,13 @@ Ltac block_goal := match goal with [ |- ?T ] => change (block T) end.
 Ltac unblock_goal := unfold block in *.
 
 
-(** [select] finds the first hypothesis matching [pat] and passes it
-to the continuation [tac]. Its main advantage over using [match goal
-with ] directly is that it is shorter. If [pat] matches multiple
-hypotheses, then [tac] will only be called on the first matching
-hypothesis. If [tac] fails, [select] will not backtrack on subsequent
-matching hypotheses.
-
-[select] is written in CPS and does not return the name of the
+(** The tactic [select pat tac] finds the last (i.e., bottommost) hypothesis
+matching [pat] and passes it to the continuation [tac]. Its main advantage over
+using [match goal with ] directly is that it is shorter. If [pat] matches
+multiple hypotheses and [tac] fails, then [select tac] will not backtrack on
+subsequent matching hypotheses.
+
+The tactic [select] is written in CPS and does not return the name of the
 hypothesis due to limitations in the Ltac1 tactic runtime (see
 https://gitter.im/coq/coq?at=5e96c82f85b01628f04bbb89). *)
 Tactic Notation "select" open_constr(pat) tactic3(tac) :=