diff --git a/theories/tactics.v b/theories/tactics.v
index 203aa30b9008a9cc5e98cec4ed62e94409a0d0dd..54e8189ca0462fa1b1fe1325117bf8e9c26f9d23 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -519,7 +519,11 @@ 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) :=
   lazymatch goal with
-  (* The [unify] is necessary, otherwise holes in [pat] stay as side-conditions *)
+  (** Before running [tac] on the hypothesis [H] we must first unify the
+      pattern [pat] with the term it matched against. This forces every evar
+      coming from [pat] (and in particular from the holes [_] it contains and
+      from the implicit arguments it uses) to be instantiated. If we do not do
+      so then shelved goals are produced for every such evar. *)
   | H : pat |- _ => let T := (type of H) in unify T pat; tac H
   end.
 (** [select_revert] reverts the first hypothesis matching [pat]. *)