Expand comment in `select`; based on `iSelect` in Iris.

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]. *)