From cf9f43cb9f8256fa1803ff366dd565d33990b49d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 27 Jan 2021 18:02:23 +0100
Subject: [PATCH] Expand comment in `select`; based on `iSelect` in Iris.

---
 theories/tactics.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index 203aa30b..54e8189c 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]. *)
-- 
GitLab