Fix documentation of `select` to state that it selects the "last" hypothesis.

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.

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) :=